An Interactive Theorem Prover Implemented in Teyjus

The code accessible from this page shows the implementation of an interactive theorem prover based on tactics and tacticals in Teyjus. This code brings out many of the good features of Lambda Prolog: lambda terms as a means for capturing the higher-order abstract syntax of formulas and proofs, beta conversion as a means for realizing substitution correctly, benefits of higher-order programming and the support for search in logic programming as a natural basis for realizing tactics and tacticals. The menu below provides some help in understanding the structure of the code.

Encodings for formulas and proofs in a first order logic
- Sorts and contants encoding the logical and nonlogical vocabulary of a first-order logic.
- Illustrations of the encodings of formulas
- Encodings of proofs in a natural deduction calculus
Implementation of tactics and tacticals
- Encodings of goals in theorem proving
- Signature and code realizing some primitive tactics (Signature and code for list manipulation routines used in this code)
- Signature and code for goal simplification code
- Signature and code for some tacticals
Signature and code for the interactive theorem prover
Script illustrating the use of the code
Download a tarred version of all the code

The code in this directory is based on work in the doctoral dissertation of Amy Felty and has been adapted to Teyjus from an demo of the first implementation of Lambda Prolog.

Last changed by gopalan@cs.umn.edu on August 12, 2003