He, LiFeng; Chao, Yuyan; Nakamura, Tsuyoshi; Itoh, Hidenori \(\mathcal I\)-SATCHMORE: An improvement of \(\mathcal A\)-SATCHMORE. (English) Zbl 1089.68625 J. Comput. Sci. Technol. 18, No. 2, 181-189 (2003). 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. Cited in 1 Document MSC: 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) Keywords:theorem proving; availability; forward chaining; SATCHMO; SATCHMORE; \(\mathcal A\)-SATCHMORE Software:SATCHMO; TPTP PDFBibTeX XMLCite \textit{L. He} et al., J. Comput. Sci. Technol. 18, No. 2, 181--189 (2003; Zbl 1089.68625) 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.