[ Home
| Overview
| Download
| Language Documentation
| Bug Tracking
| Implementation
Documentation
| Links ]
#
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

- Analyzing formula structure

- Analysis and synthesis of formula structure

- 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

[ Home
| Overview
| Download
| Language Documentation
| Bug Tracking
| Implementation
Documentation
| Links ]

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