Ergo 6: a generic proof engine that uses Prolog proof technology
Mark Utting, Peter Robinson and Ray Nickson
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.
|
