×
Schütz, Heribert; Geisler, Tim

Efficient model generation through compilation. (English) Zbl 1045.68605

Inf. Comput. 162, No. 1-2, 138-157 (2000).
Summary: We present a collection of simple but powerful techniques for enhancing the efficiency of tableau-based model generators 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 have compared various combinations of our techniques among each other and with theorem provers based on various calculi, 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 nonnesting.

Cited in 1 Document

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
68N20 Theory of compilers and interpreters

Keywords:

tableau-based model generators; Satchmo; TPTP problem library

Software:

SETHEO; SATCHMO; TPTP; PTTP
Cite Review PDF
Full Text: DOI

References:

[1] Bancilhon, F.; Ramakrishnan, R., An amateur’s introduction to recursive query processing strategies, Proc. ACM SIGMOD 1986 (1987), Assoc. Comput. Mach: Assoc. Comput. Mach New York, p. 16-52
[2] Baumgartner, P.; Furbach, U.; Niemelä, I., Hyper tableaux, Logics in Artificial Intelligence: European Workshop, JELIA ’96. Logics in Artificial Intelligence: European Workshop, JELIA ’96, Lecture Notes Artificial Intelligence, 1126 (1996), Springer-Verlag: Springer-Verlag Berlin/New York · Zbl 1427.03031
[3] Bayer, R., Query Evaluation and Recursion in Deductive Database Systems, Technical Report (1985)
[4] Beckert, B.; Posegga, J., lean\(T^AP\): lean, tableau-based theorem proving, (Bundy, A., 13th Int. Conf. on Automated Deduction (CADE), Nancy, France, June/July 1994. 13th Int. Conf. on Automated Deduction (CADE), Nancy, France, June/July 1994, Lecture Notes in Artificial Intelligence, 814 (1994), Springer-Verlag: Springer-Verlag Berlin/New York) · Zbl 1433.68534
[5] Bry, F.; Yahya, A., Minimal model generation with positive unit hyper-resolution tableaux, 5th Workshop on Theorem Proving with Tableaux and Related Methods. 5th Workshop on Theorem Proving with Tableaux and Related Methods, Lecture Notes in Artificial Intelligence, 1071 (1996), Springer-Verlag: Springer-Verlag Berlin/New York, p. 143-159 · Zbl 1412.68212
[6] Caferra, R.; Zabel, N., Extending resolution for model construction, Logics in AI: European Workshop JELIA ’90. Logics in AI: European Workshop JELIA ’90, Lecture Notes in Artificial Intelligence, 78 (1991), Springer-Verlag: Springer-Verlag Berlin/New York, p. 153-169 · Zbl 0797.03009
[7] Denecker, M.; De Schreye, D., On the duality of abduction and model generation, (Staff, I., Proceedings, International Conference on Fifth Generation Computer Systems ’92 (1992), IOS Press: IOS Press Amsterdam), 650-657 · Zbl 0862.68019
[8] Fermüller, C.; Leitsch, A., Hyperresolution and automated model building, J. Logic Comput., 6, 173-203 (1996) · Zbl 0861.68086
[9] Forgy, C., A fast algorithm for the many patterns/many objects pattern match problem, Artificial Intelligence, 19, 17-37 (1982)
[10] Fujita, H.; Hasegawa, R., A model generation theorem prover in KL1 using a ramified-stack algorithm, Logic Programming, Proc. of the 8th Int. Conf. (1991), p. 535-548
[11] Goller, C.; Letz, R.; Mayr, K.; Schumann, J., SETHEO V3.2: Recent developments, Automated Deduction-CADE-12. Automated Deduction-CADE-12, Lecture Notes in Artificial Intelligence, 814 (1994), Springer-Verlag: Springer-Verlag Berlin/New York, p. 778-782
[12] Graf, P.1995, Term Indexing, Ph.D. thesis, Universität des Saarlandes, 1995. [Lecture Notes in Artificial Intelligence, Vol. 1053, Springer-Verlag, Berlin/New York].; Graf, P.1995, Term Indexing, Ph.D. thesis, Universität des Saarlandes, 1995. [Lecture Notes in Artificial Intelligence, Vol. 1053, Springer-Verlag, Berlin/New York]. · Zbl 0970.68152
[13] Herr, L., Rapport de stage de D.E.A. (1993)
[14] Model Generation Theorem Prover: MGTP (1995)
[15] Loveland, D. W.; Reed, D. W.; Wilson, D. S., SATCHMORE: SATCHMO with Relevancy, J. Automat. Reason., 14, 325-351 (1995) · Zbl 0939.68824
[16] Manthey, R.; Bry, F., SATCHMO: A theorem prover implemented in Prolog, 9th Int. Conf. on Automated Deduction (CADE). 9th Int. Conf. on Automated Deduction (CADE), Lecture Notes in Computer Science, 310 (1988), Springer-Verlag: Springer-Verlag Berlin/New York, p. 415-434 · Zbl 0668.68104
[17] McCune, W. W., Technical Report (1994)
[18] Posegga, J., Compiling proof search in semantic tableaux, Proc. 7th International Symposium on Methodologies for Intelligent Systems (ISMS). Proc. 7th International Symposium on Methodologies for Intelligent Systems (ISMS), Lecture Notes in Computer Science, 671 (1993), Springer-Verlag: Springer-Verlag Berlin/New York, p. 67-77
[19] Sahlin, D. 1991, An Automatic Partial Evaluator for Full Prolog, SICS Dissertation Series 04, The Royal Institute of Technology (KTH), Stockholm, 1991.; Sahlin, D. 1991, An Automatic Partial Evaluator for Full Prolog, SICS Dissertation Series 04, The Royal Institute of Technology (KTH), Stockholm, 1991.
[20] Schütz, H., Tuple-oriented Bottom-up Evaluation of Logic Programs (1993), Technische Universität München
[21] Slaney, J., Technical Report (1992)
[22] Stickel, M. E., A Prolog technology theorem prover: Implementation by an extended Prolog compiler, J. Automat. Reason., 4, 353-380 (1988) · Zbl 0662.68104
[23] Sutcliffe, G.; Suttner, C.; Yemenis, T., The TPTP problem library, Automated Deduction—CADE-12. Automated Deduction—CADE-12, Lecture Notes Artificial Intelligence, 814 (1994), Springer-Verlag: Springer-Verlag Berlin/ New York, p. 252-266 · Zbl 1433.68569
[24] Suttner, C. B.; Slaney, J., The design of the CADE-13 ATP system competition, 13th Int. Conf. on Automated Deduction (CADE). 13th Int. Conf. on Automated Deduction (CADE), Lecture Notes in Artificial Intelligence, 1104 (1996), Springer-Verlag: Springer-Verlag Berlin/New York, p. 146-160 · Zbl 1412.68263
[25] Tammet, T., Using resolution for deciding solvable classes and building finite models, Baltic Computer Science: selected papers. Baltic Computer Science: selected papers, Lecture Notes in Computer Science, 502 (1991), Springer-Verlag: Springer-Verlag Berlin/New York, p. 33-64 · Zbl 1412.68264
[26] Wunderwald, J. E., Memoring evaluation by source-to-source transformation, Fifth Int. Workshop on Logic Program Synthesis and Transformation (LOPSTR ’95). Fifth Int. Workshop on Logic Program Synthesis and Transformation (LOPSTR ’95), Lecture Notes in Computer Science, 1048 (1996), Springer-Verlag: Springer-Verlag Berlin/New York, p. 17-32
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.