Skip to main content

A Tactic Language for Ergo

A. Martin‚ R. Nickson and M. Utting

Abstract

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.

Address
Singapore
Book Title
Formal Methods Pacific '97
Editor
Lindsay Groves and Steve Reeves
ISBN
981−3083−31−X
Keywords
tactics‚user interface
Month
jul
Note
Also appears as TR97−16‚ Software Verification Research Centre‚ The University of Queensland‚ QLD 4072‚ Australia
Publisher
Springer−Verlag
Series
Springer Series in Discrete Mathematics and Theoretical Computer Science
Year
1997