LMA/ITP. Logic Machine Architecture
Ewing L. Lusk, Ross Overbeek · OSTI OAI (U.S. Department of Energy Office of Scientific and Technical Information) · 1984
LMA (Logic Machine Architecture) is a set of software tools for the construction of automated reasoning systems. It is a layered architecture for the creation of inference engines. Layer 1 of the architecture supports the functions required to maintain a database of logical formulas. Layer 2 includes the functions required to construct clause-based reasoning systems, such as ITP. LMA includes most resolution inference mechanisms, paramodulation, demodulation, subsumption, weighting, and a variety of other features. This release is identified by the authors as version 2.0 of LMA. It was developed with the explicit goal of avoiding restrictions on items such as literals/clause, variables/clause, etc. ITP, an example interactive theorem prover implemented using the LMA tools, is in itself adequate for many research and educational purposes. ITP, in LMA terminology, is considered a Layer 3 program. ITP is a clause-based reasoning system supporting a wide variety of techniques which have proven valuable over the years in a long-running automated deduction research project. In addition, it is designed to present a convenient, interactive interface to its user.