Some Formula Manipulating Programs in Teyjus

The code accessible from this page illustrates the use of higher-order abstract syntax as it is supported in Lambda Prolog in representing and manipulating formulas in quantificational logic. One component to understand here is the way formulas are encoded. Three manipulation tasks are also considered and these illustrate the benefits of beta reduction in realizing substitution into formulas, of higher-order unification in probing formula structure and of the new scoping primitives in Lambda Prolog in carrying out computations over abstraction structure. The menu below provides some help in understanding the structure of the code.

Term encodings for formulas in a first order logic
Implementing a Horn clause logic interpreter
- Signature and code for the interpreter
- Signature and code for a testing harness
Analyzing formula structure
- Signature and code for recognizing terms and quantifier free formulas
- Signature and code for recognizing goals and clauses in Horn clause logic
- Signature and code for a testing harness
Analysis and synthesis of formula structure
- Signature and code for a transformer to prenex normal form
- Signature and code for a testing harness
Scripts illustrating the use of the code
Download a tarred version of all the code

The code in this directory is adapted by Gopalan Nadathur from material in the paper ``Higher-Order Logic Programming'' by Gopalan Nadathur and Dale Miller

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