Abstract
Satchmo is a theorem prover consisting of just a few short and simple Prolog programs. Prolog may be used for representing problem clauses as well. SATCHMO is based on a model-generation paradigm. It is refutation-complete if used in a level-saturation manner. The paper provides a thorough report on experiences with SATCHMO. A considerable amount of problems could be solved with surprising efficiency.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Bry, F. et. al., A Uniform Approach to Constraint Satisfaction and Constraint Satisfiability in Deductive Databases, ECRC Techn. Rep. KB-16, 1987 (to appear in Proc. Int. Conf. Extending Database Technology EDBT 88)
Butler, R. et al., Paths to High-Performance Automated Theorem Proving, Proc. 8th CADE 1986, Oxford, 1986, 588–597
Lusk, E. and Overbeek, R., Non-Horn problems, Journal of Automated Reasoning 1 (1985), 103–114
Manthey, R. and Bry, F., A hyperresolution-based proof procedure and its implementation in PROLOG, Proc. of GWAI-87 (11th German Workshop on Artificial Intelligence), Geseke, 1987, 221–230
McCune, B., A Proof of a Non-Obvious Theorem, AAR Newsletter No. 7, 1986, 5
Nicolas, J.M., Logic for improving integrity checking in relational databases, Tech. Rep., ONERA-CERT, Toulouse, Feb. 1979 (also in Acta Informatica 18, 3, Dec. 1982)
Ohlbach, H.J. and Schmidt-Schauss, M., The Lion and the Unicorn, J. of Automated Reasoning 1 (1985), 327–332
Pelletier, F.J., Seventy-five Problems for Testing Automatic Theorem Provers, J. of Automated Reasoning 2 (1986), 191–216
Pelletier, F.J. and Rudnicki, P., Non-Obviousness, AAR Newsletter No. 6, 1986, 4–5
Smullyan, R., First-Order Logic, Springer-Verlag, 1968
Stickel, M., A Prolog Technology Theorem Prover, New Generation Computing 2, (1984), 371–383
Stickel, M., Schubert's steamroller problem: formulations and solutions, J. of Automated Reasoning 2 (1986), 89–101
Walther, C., A mechanical solution of Schubert's steamroller by many-sorted resolution, Proc. of AAAI-84, Austin, Texas, 1984, 330–334 (Revised version in Artificial Intelligence, 26, 1985, 217–224)
Walther, C., An Obvious Solution for a Non-Obvious Problem, AAR Newsletter No. 9, Jan. 1988, 4–5
Wos, L. et. al., Automated Reasoning, Prentice Hall, 1984
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1988 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Manthey, R., Bry, F. (1988). SATCHMO: A theorem prover implemented in Prolog. In: Lusk, E., Overbeek, R. (eds) 9th International Conference on Automated Deduction. CADE 1988. Lecture Notes in Computer Science, vol 310. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0012847
Download citation
DOI: https://doi.org/10.1007/BFb0012847
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-19343-2
Online ISBN: 978-3-540-39216-3
eBook Packages: Springer Book Archive