Abstract
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.
Recommended Citation
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
Department(s)
Computer Science
International Standard Book Number (ISBN)
978-089791502-1
Document Type
Article - Conference proceedings
Document Version
Citation
File Type
text
Language(s)
English
Rights
© 2023 Association for Computing Machinery, All rights reserved.
Publication Date
01 Jan 1992
