The Programmable Strategy Theorem Prover: An Implementation of the Linear MESON Procedure
Abstract
The Programmable Strategy Theorem Prover (PSIP) is a theorem proving program for the first order predicate calculus using the linear MESON procedure as the inference system. The linear MESON procedure is a new variant of the model elimination theorem proving procedure for theories with or without equality which is an affirmation rather than a refutation procedure. It is profitably viewed as an extension of the problem-reduction method. The fundamental element of a linear MESON procedure deduction, the chain, is a representation of a set of goals to be solved and their supergoals.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jun 01, 1974
- Accession Number
- ADA004474
Entities
People
- Mark E. Stickel
Organizations
- Carnegie Mellon University