CMU Artificial Intelligence Repository
Qu-Prolog and Ergo: Prototyping of Interactive Theorem
Provers
areas/reasonng/atp/systems/qu_pl/
Qu-Prolog is a high-level language designed primarily for rapid
prototyping of interactive theorem provers and, more generally, for
symbolic computation on formal languages. Its object level includes
quantified terms and object variables. As an example, the interactive
theorem prover Ergo 4.0 is implemented in Qu-Prolog. The compactness
and high level of Ergo 4.0 source code demonstrate the advantages of
Qu-Prolog for such applications. Ergo includes a 'window inference'
method that is specifically designed to support hierarchical
goal-directed proofs and allow easy access to the context of a
subterm. Ergo also provides support for defining a variety of logics
and support for proving schematic theorems and answer extraction.
Ergo is being used to support the development of verified software.
Origin:
ftp.cs.uq.oz.au:/pub/SVRC/software/qp.tar.Z
ftp.cs.uq.oz.au:/pub/SVRC/software/Ergo.tar
ftp.cs.uq.oz.au:/pub/SVRC/techreports/tr93-18.ps.Z
Problems with the ftp site should be directed to
svrctr@cs.uq.oz.au.
Version: Qu-Prolog 3.2 (7-DEC-93); Ergo 4.0 (9-DEC-93)
Ports: The system has been tested only on a Sun4.
CD-ROM: Prime Time Freeware for AI, Issue 1-1
Author(s): Peter Robinson
Keywords:
Authors!Robinson, Automated Reasoning, Ergo, Qu-Prolog,
Reasoning!Automated Reasoning, Theorem Proving, Verification
References: ?
Last Web update on Mon Feb 13 10:27:38 1995
AI.Repository@cs.cmu.edu