Skip to main content
SpringerLink
Log in

Eliminating redundant search space on backtracking for forward chaining theorem proving

  • Published:
Journal of Computer Science and Technology Aims and scope Submit manuscript

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Manthey R, Bry F. SATCHMO: A theorem prover implemented in Prolog. InProc. 9th Intl. Conf. Automated Deduction, Argonne, USA, 1988, pp.415–434.

  2. Ramsay A. Generating relevant models.Journal of Automated Reasoning, 1991, 7: 359–368.

    Article  MATH  MathSciNet  Google Scholar 

  3. Loveland D W, Reed D W, Wilson D S. SATCHMORE: SATCHMO with RElevancy.Journal of Automated Reasoning, 1995, 14: 325–351.

    Article  MATH  MathSciNet  Google Scholar 

  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. 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.

    MATH  MathSciNet  Google Scholar 

  6. He L.I-SATCHMO: An improvement of SATCHMO.Journal of Automated Reasoning, 2001, 27: 313–322.

    Article  MATH  MathSciNet  Google Scholar 

  7. Sutcliffe G, Suttner C. The TPTP problem library for automated theorem proving. http://www.cs.miami. edu/~tptp/

  8. He L. UNSEARCHMO: Eliminating redundant search space on backtracking for forward chaining theorem proving. InIJCAI'2001, Seatle, USA, 2001, pp.618–623.

  9. Bry F, Yahya A. Positive unit hyperresolution tableaux and their application to minimal model generation.Journal of Automated Reasoning, 2000, 25: 35–82.

    Article  MATH  MathSciNet  Google Scholar 

  10. Stickel M E. Schubert's steamroller problem: Formulations and solutions.J. of Automated Reasoning, 1986, 2: 89–101.

    Article  MATH  MathSciNet  Google Scholar 

  11. Chou S, Gao X, Zhang J. A deductive database to automated geometry theorem proving.Journal of Automated Reasoning, 2000, 25: 219–246.

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Faculty of Information Science and Technology, Aichi Prefectural University, 480-1198, Aichi, Japan

    Lifeng He

  2. Faculty of Environment, Information and Business, Nagoya Sangyo University, 488-8711, Aichi, Japan

    Yuyan Chao

  3. Department of Artificial Intelligence and Computer Science, Nagoya Institute of Technology, 466-8555, Nagoya, Japan

    Hidenori Itoh

Authors
  1. Lifeng He
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Yuyan Chao
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Hidenori Itoh
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Lifeng He.

Additional information

This research is partially supported by the Japan Society for the Promotion of Science under Grant No.12AI-320-2.

Lifeng He received the Ph.D. degree from Nagoya Institute of Technology, Japan, in 1997. Since 1999, he has been an associate professor at Aichi Prefectural University, Japan. His research interests include automated reasoning, theorem proving, knowledge bases, multi-agent system and image processing.

Yuyan Chao received the Ph.D. degree from Nagoya University, Japan, in 2000. From Apr. 2000 to Mar. 2002, she was a postdoctoral fellow of Nagoya Institute of Technology. From Apr. 2002 to Sept. 2002, she was a postdoctoral fellow of the Japan Society of the Promotion of Science. She is currently a lecturer at Nagoya Sangyo University. Her research interests include automated reasoning, graphic understanding, CAD and image processing.

Hidenori Itoh received the Ph.D. degree from Nagoya University, Japan, in 1974. From 1974 to 1985, he worked at Nippon Telephone and Telegraph Laboratories (NTT). From 1985 to 1989, he was with the Institute for New Generation Computer Technology (ICOT). Since 1989, he has been a professor at the Nagoya Institute of Technology. His current research interests include multimedia, artificial life and AI.

Rights and permissions

Reprints and permissions

About this article

Cite this article

He, L., Chao, Y. & Itoh, H. Eliminating redundant search space on backtracking for forward chaining theorem proving. J. Comput. Sci. & Technol. 18, 580–591 (2003). https://doi.org/10.1007/BF02947117

Download citation

  • Received:

  • Revised:

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF02947117

Keywords

Search

Navigation