Satchmo [MA88] is a Theorem Prover Implemented in Prolog Which Attempts to Provide Satisfiability Checking through Model Generation. This Paper Gives a Brief Introduction to SATCHMO and Reports Extensions to the Original Work Which Allow SATCHMO to Solve Problems Previously Considered to Be Finitely Unprovable within the SATCHMO System. the Specific Problems Are from [PE86, MO85, LU85] and Were Designed to Convert Simple Propositional Logic Problems into Functionally Difficult First Order Problems. Although the Benefits of using the SATCHMO System Are Many, the Fact that It Could Not Offer Proofs for a Set of Problems Provable in Other Systems is Troublesome, Especially in Light of the Claim that the System is Correct and Complete. This Paper Shows that SATCHMO Can in Fact, Generate These Proofs When the Problems Are Correctly Represented.
R. Rankin and R. W. Wilkerson, "Proving Functionally Difficult Problems through Model Generation," Applied Computing: Technological Challenges of the 1990's, pp. 526 - 529, Association for Computing Machinery, Jan 1992.
The definitive version is available at https://doi.org/10.1145/143559.150707
International Standard Book Number (ISBN)
Article - Conference proceedings
© 2023 Association for Computing Machinery, All rights reserved.
01 Jan 1992