Skip to main content
SpringerLink
Log in
Book cover

International Conference on Computer Logic

COLOG 1988: COLOG-88 pp 327–338Cite as

A proof-search method for the first order logic

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 417))

Abstract

A new proof search method for the first order logic based on Gentzen-like calculus is presented. Neither conjunctive nor disjunctive normal forms are used. Soundness and completeness of some strategies are proved. The method essentially uses the general ideas of Maslov's inverse method [8].

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Andrews P.B.: Theorem proving via general matings. J.Assoc. Comp. Math. 2(1981), v.28, 193–214

    Google Scholar 

  2. Bibel W.: Automated theorem proving. Vieweg Verlag, (1982)

    Google Scholar 

  3. de Champeaux D.: Sub-problem finder and instance checker: two cooperating preprocessors for theorem-provers. 6th IJCAI, (1981), v.1, 191–196

    Google Scholar 

  4. Chang C., Lee R.C.: Symbolic logic and mechanical theorem proving. Academic Press, (1973)

    Google Scholar 

  5. Dragalin A.: A proof-search method. Proc. 8th Int. Congress on Logic, Methodology and Philosophy of Sci. Moscow, (1987)

    Google Scholar 

  6. Gentzen G.: Untersuchungen uber das logishe Schliessen. Math. Z. (1935), v.39, 176–210; 405–431

    Google Scholar 

  7. Loveland D.: Automated theorem proving: a logical basis. North Holland, (1978)

    Google Scholar 

  8. Maslov S.Y.: Inverse method of establishing deducibility for logical calculi. Trudy Math. Inst. (1968), v.98

    Google Scholar 

  9. Schutte K.: Beweistheorie. Springer Verlag, (1960)

    Google Scholar 

  10. Stickel M.: A Prolog technology theorem prover. 8th International Conf. on Automated Deduction, Lecture Notes in Comput. Sci. (1986), v.230

    Google Scholar 

  11. Voronkov A.A.: A proof search method. Vychislitelnye sistemy, Novosibirsk, (1985), v.107, 109–124 (in Russian)

    Google Scholar 

  12. Voronkov, A.A.: Degtjarev A.I.: Automated theorem proving I, II. Kibernetika, (1986), v.3, (1987) v.4 (In Russian)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Mathematics, 630090, Novosibirsk 90, USSR

    A. A. Voronkov

Authors
  1. A. A. Voronkov
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Per Martin-Löf Grigori Mints

Rights and permissions

Reprints and permissions

Copyright information

© 1990 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Voronkov, A.A. (1990). A proof-search method for the first order logic. In: Martin-Löf, P., Mints, G. (eds) COLOG-88. COLOG 1988. Lecture Notes in Computer Science, vol 417. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52335-9_63

Download citation

  • DOI: https://doi.org/10.1007/3-540-52335-9_63

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-52335-2

  • Online ISBN: 978-3-540-46963-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation