CMU Artificial Intelligence Repository
Home INFO Search FAQs Repository Root

Qu-Prolog and Ergo: Prototyping of Interactive Theorem Provers

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.
   Problems with the ftp site should be directed to

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