Abstract: 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.
Publication Year: 1982
Publication Date: 1982-12-01
Language: en
Type: article
Access and Citation
Cited By Count: 15
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot