An LMA-Based Theorem Prover
Ewing L. Lusk, Ross Overbeek · CERN Document Server (European Organization for Nuclear Research) · 1982
We describe here a theorem prover constructed from the facilities provided by Logic Machine Architecture (LMA). This program is not part of LMA itself, but illustrates the level of inference-based system which can be constructed from the LMA package of tools. It is a clause-based theorem prover 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 which includes a number of useful utility commands.