Skip to main content
SpringerLink
Log in

An Improvement of Herbrand's Theorem and Its Application to Model Generation Theorem Proving

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

Abstract

This paper presents an improvement of Herbrand’s theorem. We propose a method for specifying a sub-universe of the Herbrand universe of a clause set \( {\mathcal{S}} \) for each argument of predicate symbols and function symbols in \( {\mathcal{S}} \). We prove that a clause set \( {\mathcal{S}} \) is unsatisfiable if and only if there is a finite unsatisfiable set of ground instances of clauses of \( {\mathcal{S}} \) that are derived by only instantiating each variable, which appears as an argument of predicate symbols or function symbols, in \( {\mathcal{S}} \) over its corresponding argument's sub-universe of the Herbrand universe of \( {\mathcal{S}} \). Because such sub-universes are usually smaller (sometimes considerably) than the Herbrand universe of \( {\mathcal{S}} \), the number of ground instances may decrease considerably in many cases. We present an algorithm for automatically deriving the sub-universes for arguments in a given clause set, and show the correctness of our improvement. Moreover, we introduce an application of our approach to model generation theorem proving for non-range-restricted problems, show the range-restriction transformation algorithm based on our improvement and provide examples on benchmark problems to demonstrate the power of our approach.

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.

Similar content being viewed by others

References

  1. Herbrand J. Recherches sur la théorie de la démonstration [Dissertation]. University of Paris, 1930.

  2. Gilmore P C. A proof method for quantification theory: Its justification and realization. IBM J. Res. Develop. 1960, pp.28~35.

  3. Manthey R, Bry F. SATCHMO: A theorem prover implemented in Prolog. In Proc. 9th Int. Conf. Automated Deduction, Argonne, Illinois, USA, 1988, pp.415~434.

    Chapter  Google Scholar 

  4. Bry F, Yahya A. Positive unit hyperresolution tableaux and their application to minimal model generation. J. Automated Reasoning, 2000, 25(1): 35~82.

    Article  MATH  MathSciNet  Google Scholar 

  5. Stickel M E. Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction. J. Automated Reasoning, 1994, 13(2): 189~210.

    Article  MATH  MathSciNet  Google Scholar 

  6. Geisler T, Panne S, Schutz H. Satchmo: The compiling and functional variants. J. Automated Reasoning, 1997, 18(2): 227~236.

    Article  Google Scholar 

  7. Loveland D W, Reed D W, Wilson D S. SATCHMORE: SATCHMO with RElevancy. J. Automated Reasoning, 1995, 14(2): 325~351.

    Article  MATH  MathSciNet  Google Scholar 

  8. He L, Chao Y, Simajiri Y et al. \( {\user1{\mathcal{A}}} \)-SATCHMORE: SATCHMORE with availability checking. New Generation Computing, 1998, 16(1): 55~74.

    Article  Google Scholar 

  9. He L. I-SATCHMO: An Improvement of SATCHMO. J. Automated Reasoning, 2001, 27(3): 313~322.

    Article  MATH  Google Scholar 

  10. He L, Chao Y, Nakamura T et al. \( {\user1{\mathcal{I}}} \)-SATCHMORE: An improvement of \( {\user1{\mathcal{A}}} \)-SATCHMORE. J. Comput. Sci. & Technol., 2003, 18(2): 181~189.

    MATH  MathSciNet  Google Scholar 

  11. He L, Chao Y, Itoh H. R-SATCHMO: Refinements on I-SATCHMO. J. Logic and Computation, 2004, 14(2): 117~143.

    Article  MATH  MathSciNet  Google Scholar 

  12. Loveland D W, Yahya A H. SATCHMOREBID: SATCHMO(RE) with BIDirectional relevancy. New Generation Computing, 2003, 21(3): 175~206.

    Google Scholar 

  13. Schulz S. A comparison of different techniques for grounding near-propositional CNF formulae. In Proc. the 15th FLAIRS, London, 2002, pp.72~76.

  14. Lee S J, Plaisted D A. Eliminating duplication with the hyper-linking strategy. J. Automated Reasoning, 1992, 9(1): 25~42.

    Article  MATH  MathSciNet  Google Scholar 

  15. Yu Q, Almulla M, Newborn M. Heuristics used by HERBY for semantic tree theorem proving. Ann. Math. Artif. Intell., 1998, 23(3/4): 247~266.

    Article  MATH  Google Scholar 

  16. Chang C L, Lee K C T. Symbolic Logic and Mechanical Theorem Proving. New York: Academic Press, 1997.

    Google Scholar 

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

    Google Scholar 

  18. Robinson J A. A machine-oriented logic based on the resolution principle. J. ACM, 1965, 12(1): 23~41.

    Article  MATH  Google Scholar 

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

  20. The CADE ATP System Competition held at the Third International Joint Conference on Automated Reasoning, Seattle, USA, 2006. http://www.cs.miami.edu/~tptp/CASC/J3/

  21. Schutz H, Geisler T. Efficient model generation through compilation. Information and Computation, 2000, 162(2): 138~157.

    Article  MathSciNet  Google Scholar 

  22. Morales J, Carro M, Hermenegildo M. Improving the compilation of Prolog to C using type and determinism information: Preliminary results. In Proc. Colloquium on Implementation of Constraint and Logic Programming Systems (ICLP Associated Workshop), Mumbai, India, December 2003, pp.89~102.

Download references

Author information

Authors and Affiliations

  1. Graduate School of Environment Management, Nagoya Sangyo University, Aichi, Japan

    Yu-Yan Chao

  2. College of Mechanical and Electrical Engineering, Shaanxi University of Science and Technology, Shaanxi, China

    Yu-Yan Chao

  3. Graduate School of Information Science and Technology, Aichi Prefectural University, Aichi, Japan

    Li-Feng He

  4. College of Computer and Information Engineering, Shaanxi University of Science and Technology, Shaanxi, China

    Li-Feng He

  5. Graduate School of Computer Science and Engineering, Nagoya Institute of Technology, Nagoya, Japan

    Tsuyoshi Nakamura, Zheng-Hao Shi & Hidenori Itoh

  6. Department of Radiology, The University of Chicago, Chicago, USA

    Kenji Suzuki

  7. Currently, Research Associate, The University of Chicago, Chicago, USA

    Li-Feng He

Authors
  1. Yu-Yan Chao
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Li-Feng He
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Tsuyoshi Nakamura
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Zheng-Hao Shi
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Kenji Suzuki
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Hidenori Itoh
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Yu-Yan Chao.

Additional information

This work was supported partially by TOYOAKI Scholarship Foundation, Japan.

Electronic supplementary material

Rights and permissions

Reprints and permissions

About this article

Cite this article

Chao, YY., He, LF., Nakamura, T. et al. An Improvement of Herbrand's Theorem and Its Application to Model Generation Theorem Proving. J Comput Sci Technol 22, 541–553 (2007). https://doi.org/10.1007/s11390-007-9062-2

Download citation

  • Received:

  • Revised:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11390-007-9062-2

Keywords

Search

Navigation