×

zbMATH — the first resource for mathematics

A tactic language for Ergo. (English) Zbl 0886.68124
Groves, Lindsay (ed.) et al., Formal methods Pacific ’97. Proceedings of FMP ’97, July 9–11, 1997, Wellington, New Zealand. Singapore: Springer. 186-207 (1997).
Summary: A new version of the Ergo theorem prover is under development. It uses a single tactic language, based on Angel, for tactic programming, user interface, and proof representation. This paper describes the language as it is used in each of these cases, and explains the details of its implementation in Qu-Prolog. An example from classical propositional calculus is included.
For the entire collection see [Zbl 0877.00014].

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Software:
Ergo 6; Qu-Prolog
PDF BibTeX XML Cite