Abstract
This paper is about automatic searching for proofs, automatic searching for models and the potentially fruitful ways in which these traditionally separate aspects of reasoning may be made to interact. It takes its starting point in research reported in 1993 (Slaney, SCOTT: A Semantically Guided Theorem Prover, Proc. 13th IJCAI) on a system which combines a high performance first order theorem prover with a program generating small models of first order theories. The main theorem is an incompleteness result for a certain range of problems to which this combined system has been successfully applied. While the result may not be unexpected, the proof is worth examining and it is important to reflect on its relationship to the research program in combining methods.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
P. Graf, Substitution tree indexing, Proceedings of the 6th Conference on Rewriting Techniques and Applications (1995).
R. Hasegawa, M. Koshimura & H. Fujita, MGTP: A Parallel Theorem Prover Based on Lazy Model Generation, Proceedings of 11th International Conference on Automated Deduction (1992), 776–780.
J.A. Kaiman, Condensed detachment as a rule of inference, Studia Logica 42 (1983), 443–451.
W. McCune, OTTER 2.0 Users Guide, Argonne National Laboratory, 1990.
W. McCune & L. Wos, Experiments in automated deduction with condensed detachment, Proceedings of 11th International Conference on Automated Deduction (1992), 209–223.
R.K. Meyer & M.W. Bunder, Condensed detachment and combinators, Technical report TR-ARP-8/88, Automated Reasoning Project, Australian National University, 1988.
R.K. Meyer, M.W. Bunder & L. Powers, Implementing the fool’s model of combinatory logic, Journal of Automated Reasoning 7 (1991).
J. Schumann, SiCoTHEO: Simple Competitive parallel Theorem Provers based on SETHE0, Typescript, Institut für Informatik, Technische Universität München, 1995.
J.R. Slagle, Automatic theorem proving with renamable and semantic resolution, Journal of the ACM 14 (1967), 687–697.
J. Slaney, SCOTT: A model-guided theorem prover, Proceedings of 13th International Joint Conference on Artificial Intelligence (1993), 109–114.
J. Slaney, FINDER: Finite Domain Enumerator (system description), Proceedings of 12th International Conference on Automated Deduction (1994), 764–768.
J. Slaney, E. Lusk & W. McCune, SCOTT:Semantically Constrained OTTER (system description)Proceedings of 12th International Conference on Automated Deduction (1994), 764–768.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1996 Springer Science+Business Media New York
About this chapter
Cite this chapter
Slaney, J., Surendonk, T. (1996). Combining Finite Model Generation with Theorem Proving. In: Baader, F., Schulz, K.U. (eds) Frontiers of Combining Systems. Applied Logic Series, vol 3. Springer, Dordrecht. https://doi.org/10.1007/978-94-009-0349-4_7
Download citation
DOI: https://doi.org/10.1007/978-94-009-0349-4_7
Publisher Name: Springer, Dordrecht
Print ISBN: 978-94-010-6643-3
Online ISBN: 978-94-009-0349-4
eBook Packages: Springer Book Archive