Journal article
Ergo 6: A Generic Proof Engine that Uses Prolog Proof Technology
LMS Journal of Computation and Mathematics, Vol.5, pp.194-219
2002
Abstract
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.
Details
- Title
- Ergo 6: A Generic Proof Engine that Uses Prolog Proof Technology
- Authors
- Mark Utting (Author) - University of Waikato, New ZealandPeter Robinson (Author) - University of QueenslandRay Nickson (Author) - Victoria University of Wellington, New Zealand
- Publication details
- LMS Journal of Computation and Mathematics, Vol.5, pp.194-219
- Publisher
- London Mathematical Society
- Date published
- 2002
- DOI
- 10.1112/S1461157000000759
- ISSN
- 1461-1570
- Organisation Unit
- School of Science and Engineering - Legacy; University of the Sunshine Coast, Queensland
- Language
- English
- Record Identifier
- 99448972402621
- Output Type
- Journal article
Metrics
674 Record Views