Abstract
We present a collection of simple but powerful techniques for enhancing the efficiency of model-generation theorem provers such as Satchmo. The central ideas are to compile a clausal first order theory into a procedural Prolog program and to avoid redundant work of a naïve implementation. We also give an efficient implementation for complement splitting, a method for minimizing the first generated model and for pruning the search space. Furthermore we show that it is not efficient to ensure fair selection of clauses by a purely breadth-first search strategy and present a significantly more efficient strategy.
We have compared various combinations of our techniques among each other and with the theorem provers MGTP/G, Otter, and SETHEO, using the TPTP Problem Library as a benchmark. Our implementation has turned out to be the most efficient for range-restricted problems and for a class of problems we call “non-nesting”.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
F. Bancilhon and R. Ramakrishnan. An amateur's introduction to recursive query processing strategies. In Proc. ACM SIGMOD 1986, pages 16–52. ACM, 1986.
R. Bayer. Query evaluation and recursion in deductive database systems. Technical Report TUM-I8503, Technische Universität München, 1985.
F. Bry and A. Yahya. Minimal model generation with positive unit hyper-resolution tableaux. In 5th Workshop on Theorem Proving with Tableaux and Related Methods, Springer LNAI, 1996.
C. Forgy. Rete: A fast algorithm for the many patterns/many objects pattern match problem. Artificial Intelligence, 19(1):17–37, 1982.
H. Fujita and R. Hasegawa. A model generation theorem prover in KL1 using a ramified-stack algorithm. In Logic Programming, Proc. of the 8th Int. Conf., pages 535–548, 1991.
C. Goller, R. Letz, K. Mayr, and J. Schumann. SETHEO V3.2: Recent devleopments. In Automated Deduction — CADE-12, Springer LNAI 814, pages 778–782, 1994.
Institute for New Generation Computer Technology. Model Generation Theorem Prover: MGTP, 1995. http://www.icot.or.jp/ICOT/IFS/IFS-abst/082.html.
R. Manthey and F. Bry. SATCHMO: A theorem prover implemented in Prolog. In 9th Int. Conf. on Automated Deduction (CADE), Springer LNCS 310, pages 415–434, 1988.
W. W. McCune. Otter 3.0 reference manual and guide. Technical Report ANL 94/6, Argonne National Laboratory, 1994.
D. Sahlin. An Automatic Partial Evaluator for Full Prolog. SICS Dissertation Series 04, The Royal Institute of Technology (KTH), 1991.
H. Schütz. Tuple-oriented Bottom-up Evaluation of Logic Programs. PhD thesis, Technische Universität München, 1993. in German.
M. E. Stickel. A Prolog technology theorem prover: Implementation by an extended Prolog compiler. Journal of Automated Reasoning, 4:353–380, 1988.
G. Sutcliffe, C. Suttner, and T. Yemenis. The TPTP problem library. In Automated Deduction — CADE-12, Springer LNAI 814, pages 252–266, 1994.
J. E. Wunderwald. Memoing evaluation by source-to-source transformation. In Fifth Int. Workshop on Logic Program Synthesis and Transformation, 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schütz, H., Geisler, T. (1996). Efficient model generation through compilation. In: McRobbie, M.A., Slaney, J.K. (eds) Automated Deduction — Cade-13. CADE 1996. Lecture Notes in Computer Science, vol 1104. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61511-3_105
Download citation
DOI: https://doi.org/10.1007/3-540-61511-3_105
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61511-8
Online ISBN: 978-3-540-68687-3
eBook Packages: Springer Book Archive