Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Sequent forms of Herbrand theorem and their applications

  • Published:
Annals of Mathematics and Artificial Intelligence Aims and scope Submit manuscript

New sequent forms* of the famous Herbrand theorem are proved for first-order classical logic without equality. These forms use the original notion of an admissible substitution and a certain modification of the Herbrand universe, which is constructed from constants, special variables, and functional symbols occurring only in the signature of an initial theory. Other well-known forms of the Herbrand theorem are obtained as special cases of the sequent ones. Besides, the sequent forms give an approach to the construction and theoretical investigation of computer-oriented calculi for efficient logical inference search in the signature of an initial theory. In a comparably simple way, they provide us with some technique for proving the completeness and soundness of the calculi.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

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

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

References

  1. J. Herbrand, Recherches sur la Theorie de la Demonstration, Travaux de la Societe des Sciences et de Lettres de Varsovie, Class III, Sciences Mathematiques et Physiques, Vol. 33 (1930) (Also see in English: Logical Writing, Hinghan, Reidel Publishing Company, 1971).

  2. A.V. Lyaletski, Variant of Herbrand theorem for formulas in prefix form (in Russian), Cybernetics 1 (1981) 112–116.

    Google Scholar 

  3. A. Lyaletski, On Herbrand theorem, The Bulletin of Symbolic Logic 7(1) (2001) 132–133.

    Google Scholar 

  4. G. Mints, Herbrand Theorem (in Russian), Mathematical Theory of Logical Inference (Nauka, Moscow, 1967) 311–350.

    Google Scholar 

  5. J.A. Robinson, A machine-oriented logic based on resolution principle, J. of the ACM 12(1) (1965) 23–41.

    Article  MATH  Google Scholar 

  6. J.H. Gallier, Logic for Computer Science: Foundations of Automatic Theorem Proving (Harper and Row, Inc., New York, 1986) 513 pp.

    MATH  Google Scholar 

  7. G. Gentzen, Untersuchungen uber das Logische Schliessen, Mathematische Zeitschrift 39 (1934) 176–210.

    Article  MathSciNet  MATH  Google Scholar 

  8. G. Takeuti, Proof Theory (North-Holland, American Elsevier Pub. Co., 1975).

  9. S. Kanger, Simplified proof method for elementary logic, Comp. Program. and Form. Sys.: Stud. in Logic (North-Holland, Pub. Co., 1963).

  10. A. Degtyarev, A. Lyaletski and M. Morokhovets, Evidence algorithm and sequent logical inference search, Lecture Notes in Artificial Intelligence 1705 (1999) 44–61.

    MathSciNet  Google Scholar 

  11. A. Lyaletski, K. Verchinine, A. Degtyarev and A. Paskevich, System for automated deduction (SAD): Linguistic and deductive peculiarities, in: Advances in Soft Computing (Intelligent Information Systems 2002, eds. M.A. Klopotek, S.T. Wierzchon and M. Michalewicz) (Physica/Springer, Berlin Heidelberg New York, 2002) 413–422.

    Google Scholar 

  12. A. Lyaletski, Computer-oriented sequent inferring without preliminary skolemization, in: Advances in Soft Computing (Intelligent Information Processing and Web Mining: Proceedings of the International IIS: IIPWM'03 Conference) (Physica/Springer, Berlin Heidelberg New York, 2003) 373–382.

  13. A. Voronkov and A. Robinson (eds.), Handbook of Automated Reasoning, Vol. I, (Elsevier Science and MIT Press, 2001) 996 pp.

  14. A. Lyaletski, Computer-oriented calculus of sequent trees, Lecture Notes in Computer Science (Foundations of Information and Knowledge Systems: Third International Symposium, FoIKS 2004), Vol. 2942 (Springer, Berlin Heidelberg New York, 2004) 213–230.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Faculty of Cybernetics, Kyiv National Taras Shevchenko University, 2, Glushkov avenue, building 6, 03022, Kyiv, Ukraine

    Alexander Lyaletski

Authors
  1. Alexander Lyaletski
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Alexander Lyaletski.

Additional information

*A part of this investigation was performed during a visit to the University of Liverpool supported by the grant NAL/00841/G given by the Nuffield foundation.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Lyaletski, A. Sequent forms of Herbrand theorem and their applications. Ann Math Artif Intell 46, 191–230 (2006). https://doi.org/10.1007/s10472-005-9017-7

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10472-005-9017-7

Keywords

AMS subject classification (2000)

Search

Navigation