CMU Artificial Intelligence Repository
Home INFO Search FAQs Repository Root

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