Ergo 6: a generic proof engine that uses Prolog proof technology. To support formal reasoning in mathematical and software engineering applications, it is desirable to have a generic prover that can be instantiated with a range of logics. This allows the prover to be applied to a wider variety of reasoning tasks than a fixed-logic prover. This paper describes the design principles and the architecture of the latest version of the Ergo proof engine, Ergo 6. Ergo 6 is a generic interactive theorem prover, similar to Isabelle, but with better support for proving schematic theorems with user-defined constraints, and with a different approach to handling variable scoping. A major theme of the paper is that Prolog implementation technology can be generalized to obtain efficient implementations of generic proof engines. This is demonstrated via a Qu-Prolog implementation of Ergo 6.
Keywords for this software
References in zbMATH (referenced in 6 articles )
Showing results 1 to 6 of 6.
- Robinson, Peter; Shankland, Carron: Combating infinite state using Ergo (2003)
- Utting, Mark; Robinson, Peter; Nickson, Ray: Ergo 6: a generic proof engine that uses Prolog proof technology (2002)
- Cerone, A.: Axiomatisation of an interval calculus for theorem proving (2001)
- Shield, J.; Hayes, I. J.; Carrington, D. A.: Using theory interpretation to mechanise the reals in a theorem prover (2001)
- Colvin, Robert; Hayes, Ian; Nickson, Ray; Strooper, Paul: A tool for logic program refinement (extended abstract) (1997)
- Martin, Andrew; Nickson, Ray; Utting, Mark: A tactic language for Ergo (1997)