×

\(\mathcal I\)-SATCHMORE: An improvement of \(\mathcal A\)-SATCHMORE. (English) Zbl 1089.68625

Summary: This paper presents an improvement of \(\mathcal A\)-SATCHMORE (SATCHMORE with availability). \(\mathcal A\)-SATCHMORE incorporates relevancy testing and availability checking into SATCHMO to prune away irrelevant forward chaining. However, considering every consequent atom of those non-Horn clauses being derivable, \(\mathcal A\)-SATCHMORE may suffer from a potential explosion of the search space when some of such consequent atoms are actually underivable. This paper introduces a solution for this problem and shows its correctness.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

SATCHMO; TPTP
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Manthey R, Bry F. SATCHMO: A theorem prover implemented in Prolog. InProc. 9th Int. Conf. on Automated Deduction, 1988. · Zbl 0668.68104
[2] Ramsay D W. Generating relevant models.Journal of Automated Reasoning, 1991, 7: 359–368. · Zbl 0733.68072 · doi:10.1007/BF00249019
[3] Loveland D W, Reed D W, Wilson D S. SATCHMORE: SATCHMO with Relevancy.Journal of Automated Reasoning, 1995, 14: 325–351. · Zbl 0939.68824 · doi:10.1007/BF00881861
[4] He L, Chao Y, Simajiri Y, Seki H, Itoh H.A-SATCHMORE: SATCHMORE with availability checking.New Generation Computing, 1998, 16: 55–74. · doi:10.1007/BF03037320
[5] Bry F, Yahya A. Positive unit hyperresolution tableaux and their application to minimal model generation.Journal of Automated Reasoning, 2000, 25: 35–82. · Zbl 0960.03006 · doi:10.1023/A:1006291616338
[6] Stickel M E. Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction.Journal of Automated Reasoning, 1994, 13: 189–210. · Zbl 0819.68113 · doi:10.1007/BF00881955
[7] Demolombe R. An efficient strategy for non-horn deductive databases.Theoretical Computer Science, 1991, 78: 245–249. · Zbl 0716.68027 · doi:10.1016/0304-3975(51)90010-2
[8] Lloyd J W. Foundations of logic programming (second Edition). Springer-Verlag, Heidelberg, 1987. · Zbl 0668.68004
[9] Chang C L, Lee K C T. Symbolic Logic and Mechanical Theorem Proving,Academic Press, New York, 1973. · Zbl 0263.68046
[10] Loveland D W. Automated Theorem Proving: A Logic Basis. North-Holland, Amsterdam, 1978. · Zbl 0364.68082
[11] Sutcliffe G, Suttner C. http://www.cs.jcu.edu.au/\(\sim\)tptp/
[12] Stickel M E. Schubert’s steamroller problem: Formulations and solutions.Journal of Automated Reasoning. 1986, 2: 89–101. · Zbl 0642.68164 · doi:10.1007/BF00246025
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.