Automated reasoning system ITP
Ewing L. Lusk, Ross Overbeek · CERN Document Server (European Organization for Nuclear Research) · 1984
This report describes a system designed to provide a portable environment for the study of automated reasoning. The system is built on the LMA automated reasoning subroutine package. This program is not part of LMA itself but illustrates the level of inference-based system that can be constructed from the LMA package of tools. It 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.