Skip to main content
SpringerLink
Log in

I-SATCHMORE: An improvement ofA-SATCHMORE

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

Abstract

This paper presents an improvement ofA-SATCHMORE (SATCHMORE with Availability).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,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.

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 Int. Conf. on Automated Deduction, 1988.

  2. Ramsay D W. 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.

    Article  Google Scholar 

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

  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.

    Article  MATH  MathSciNet  Google Scholar 

  7. Demolombe R. An efficient strategy for non-horn deductive databases.Theoretical Computer Science, 1991, 78: 245–249.

    Article  MATH  MathSciNet  Google Scholar 

  8. Lloyd J W. Foundations of logic programming (second Edition). Springer-Verlag, Heidelberg, 1987.

    MATH  Google Scholar 

  9. Chang C L, Lee K C T. Symbolic Logic and Mechanical Theorem Proving,Academic Press, New York, 1973.

    MATH  Google Scholar 

  10. Loveland D W. Automated Theorem Proving: A Logic Basis. North-Holland, Amsterdam, 1978.

    Google Scholar 

  11. Sutcliffe G, Suttner C. http://www.cs.jcu.edu.au/~tptp/

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

    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

    Chao Yuyan

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

    Nakamura Tsuyoshi & Itoh Hidenori

Authors
  1. LiFeng He
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Chao Yuyan
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Nakamura Tsuyoshi
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Itoh Hidenori
    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.

HE LiFeng received the Ph.D. degree from Nagoya Institute of Technology in 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 in Japan in 2000. From April 2000 to March 2002, she was a postdoctoral fellow of Nagoya Institute of Tecnology. From Apr. 2002 to Sept. 2002, she was a postdoctoral fellow of the Japan Society of the Promotion of Science. She is current a lecturer at Nagoya Sangyo University. Her research interests include automated reasoning, graphic understanding, CAD and image processing.

Tsuyoshi Nakamura received the Ph.D. degree from Nagoya Institute of Technology (NIT) in March 1998. He is currently a research associate at NIT. His interest and work have been in developing softcomputing applications.

Hidenori Itoh received the Ph.D. degree from Nagoya University in 1974. From 1974 to 1985, he worked at NTT. From 1985 to 1989, he was with 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., Yuyan, C., Tsuyoshi, N. et al. I-SATCHMORE: An improvement ofA-SATCHMORE. J. Comput. Sci. & Technol. 18, 181–189 (2003). https://doi.org/10.1007/BF02948883

Download citation

  • Received:

  • Revised:

  • Issue Date:

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

Keywords

Search

Navigation