Eliminating redundant search space on backtracking for forward chaining theorem proving

  • Lifeng He
  • Yuyan Chao
  • Hidenori Itoh


This paper introduces some improvements on the intelligent backtracking strategy for forward chaining theorem proving. How to decide a minimal useful consequent atom set for a refutation derived at a node in a proof tree, is discussed. In most cases, an unnecessary non-Horn clause used for forward chaining will be split only once. The increase of the search space by invoking unnecessary forward chaining clauses will be nearly linear, not exponential anymore. In this paper, the principle of the proposed method and its correctness are introduced. Moreover, some examples are provided to show that the proposed approach is powerful for forward chaining theorem proving.


theorem proving forward chaining SATCHMO I-SATCHMO model generation 


  1. [1]
    Manthey R, Bry F. SATCHMO: A theorem prover implemented in Prolog. InProc. 9th Intl. Conf. Automated Deduction, Argonne, USA, 1988, pp.415–434.Google Scholar
  2. [2]
    Ramsay A. Generating relevant models.Journal of Automated Reasoning, 1991, 7: 359–368.MATHCrossRefMathSciNetGoogle Scholar
  3. [3]
    Loveland D W, Reed D W, Wilson D S. SATCHMORE: SATCHMO with RElevancy.Journal of Automated Reasoning, 1995, 14: 325–351.MATHCrossRefMathSciNetGoogle Scholar
  4. [4]
    He L, Chao Y, Simajiri Y, Seki H, Itoh H.A-SATCHMORE: SATCHMORE with availability checking.New Generation Computing, 1998, 16: 55–74.Google Scholar
  5. [5]
    He L, Chao Y, Nakamura T, Itoh H.L-SATCHMORE: An Improvement ofA-SATCHMORE.Journal of Computer Science and Technology, 2003, 18(2): 181–189.MATHMathSciNetGoogle Scholar
  6. [6]
    He L.I-SATCHMO: An improvement of SATCHMO.Journal of Automated Reasoning, 2001, 27: 313–322.MATHCrossRefMathSciNetGoogle Scholar
  7. [7]
    Sutcliffe G, Suttner C. The TPTP problem library for automated theorem proving. edu/~tptp/Google Scholar
  8. [8]
    He L. UNSEARCHMO: Eliminating redundant search space on backtracking for forward chaining theorem proving. InIJCAI'2001, Seatle, USA, 2001, pp.618–623.Google Scholar
  9. [9]
    Bry F, Yahya A. Positive unit hyperresolution tableaux and their application to minimal model generation.Journal of Automated Reasoning, 2000, 25: 35–82.MATHCrossRefMathSciNetGoogle Scholar
  10. [10]
    Stickel M E. Schubert's steamroller problem: Formulations and solutions.J. of Automated Reasoning, 1986, 2: 89–101.MATHMathSciNetCrossRefGoogle Scholar
  11. [11]
    Chou S, Gao X, Zhang J. A deductive database to automated geometry theorem proving.Journal of Automated Reasoning, 2000, 25: 219–246.MATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Science Press, Beijing China and Allerton Press Inc. 2003

Authors and Affiliations

  1. 1.Faculty of Information Science and TechnologyAichi Prefectural UniversityAichiJapan
  2. 2.Faculty of Environment, Information and BusinessNagoya Sangyo UniversityAichiJapan
  3. 3.Department of Artificial Intelligence and Computer ScienceNagoya Institute of TechnologyNagoyaJapan

Personalised recommendations