Skip to main content
SpringerLink
Log in

Herbrand’s Theorem for Prenex Gödel Logic and Its Consequences for Theorem Proving

  • Conference paper
  • First Online:
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2001)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 2250))

Abstract

Herbrand’s Theorem for G Δ∞ , i.e., Gödel logic enriched by the projection operator Δ is proved. As a consequence we obtain a “chain normal form” and a translation of prenex G Δ∞ into (order) clause logic, referring to the classical theory of dense total orders with endpoints. A chaining calculus provides a basis for efficient theorem proving.

Partly supported by the Austrian Science Fund under grant P-12652 MAT

Research supported by EC Marie Curie fellowship HPMF-CT-1999-00301

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. A. Avron. Hypersequents, Logical Consequence and Intermediate Logics for Concurrency. Annals of Mathematics and Artificial Intelligence Vol. 4, 1991, 225–248.

    Article  MATH  MathSciNet  Google Scholar 

  2. A. Avron. The Method of Hypersequents in Proof Theory of Propositional Non-Classical Logics. In Logic: From Foundations to Applications. European Logic Colloquium, Keele, UK, July 20–29, 1993. Oxford, Clarendon Press, 1996, 1–32.

    Google Scholar 

  3. F. Baader, T. Nipkow. Term Rewriting and All That. Cambridge UP, 1998.

    Google Scholar 

  4. M. Baaz. Infinite-valued Gödel logics with 0-1-projections and relativizations. In Proceedings Gödel 96. Kurt Gödel’s Legacy. LNL 6, Springer, 23–33. 1996.

    Google Scholar 

  5. M. Baaz, A. Ciabattoni, R. Zach. Quantified Propositional Gödel Logics. In Proceedings LPAR 2000. Eds. M. Parigot, A. Voronkov LNCS 1955 Springer, 2000, 240–256

    Google Scholar 

  6. M. Baaz, U. Egly, A. Leitsch. Normal Form Transformations. Handbook of Automated Reasoning 1 Eds: A. Robinson, A. Voronkov. Elsevier, 2001, 273–333.

    Google Scholar 

  7. M. Baaz, C. Fermüller. Analytic Calculi for Projective Logics. Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX’99, LNAI 1617, Springer, 1999, 36–50.

    Google Scholar 

  8. M. Baaz, A. Leitsch, R. Zach. Incompleteness of an infinite-valued first-order Gödel Logic and of some temporal logic of programs. In: Proceedings of Computer Science Logic CSL’95. Berlin, 1996. Springer.

    Google Scholar 

  9. M. Baaz, H. Veith. Quantifier Elimination in Fuzzy Logic. Computer Science Logic, 12th International Workshop, CSL’98, LNCS 1584, 1999, 399–414.

    Google Scholar 

  10. M. Baaz, H. Veith. An Axiomatization of Quantified Propositional Gödel Logic Using the Takeuti-Titani Rule. Proc. Logic Colloquium 1998, LNML, Springer, to appear.

    Google Scholar 

  11. M. Baaz, H. Veith. Interpolation in fuzzy logic. Arch. Math. Logic, 38 (1999), 461–489.

    Article  MATH  MathSciNet  Google Scholar 

  12. M. Baaz, R. Zach. Hypersequents and the Proof Theory of Intuitionistic Fuzzy Logic. Proc. CSL’2000, 2000, 187–201.

    Google Scholar 

  13. L. Bachmair, H. Ganzinger. Ordered Chaining forTotal Orderings. Proc. CADE’94, Springer LNCS 814, 1994, 435–450.

    Google Scholar 

  14. L. Bachmair, H. Ganzinger. Ordered Chaining Calculi for First-Order Theories of Transitive Relations. J. ACM 45(6) (1998), 1007–1049.

    Article  MATH  MathSciNet  Google Scholar 

  15. A. Degtyarev, A. Voronkov. Decidability Problems for the Prenex Fragment of Intuitionistic Logic. In Proceedings LICS’96. IEEE Press, 503–509. 1996.

    Google Scholar 

  16. M. Dummett. A propositional calculus with denumerable matrix. J. Symbolic Logic, 24(1959), 97–106.

    Article  MATH  MathSciNet  Google Scholar 

  17. J.M. Dunn, R.K. Meyer. Algebraic completeness results for Dummett’s LC and its extensions. Z. Math. Logik Grundlagen Math., 17 (1971), 225–230.

    Article  MATH  MathSciNet  Google Scholar 

  18. R. Dyckhoff. A Deterministic Terminating Sequent Calculus for Gödel-Dummett Logic. Logic Journal of the IGPL, 7(1999), 319–326.

    Article  MATH  MathSciNet  Google Scholar 

  19. D.M. Gabbay. Decidability of some intuitionistic predicate theories. J. of Symbolic Logic, vol. 37, pp. 579–587. 1972.

    Article  MATH  MathSciNet  Google Scholar 

  20. H. Ganzinger, V. Sofronie-Stokkermans. Chaining Techniques for Automated Theorem Proving in Many-Valued Logics. In: Proceedings 30th IEEE Symposium on Multiple-Valued Logic. IEEE Press, 337–344. 2000.

    Google Scholar 

  21. P. Hájek. Metamathematics of Fuzzy Logic. Kluwer, 1998.

    Google Scholar 

  22. A. Horn. Logic with truth values in a linearly ordered Heyting algebra. J. Symbolic Logic, 27 (1962), 159–170.

    Article  MathSciNet  Google Scholar 

  23. A. Leitsch. The Resolution Calculus. Springer, 1997. Kluwer, 1998.

    Google Scholar 

  24. D. Plaisted, S. Greenbaum. A Structure-Preserving Clause Form Translation. J. Symbolic Computation 2 (1986), 293–304.

    Article  MATH  MathSciNet  Google Scholar 

  25. H. Rogers. Certain logical reduction and decision problems. Annals of Mathematics, vol. 64, pp. 264284. 1956.

    Article  Google Scholar 

  26. G. Takeuti, T. Titani. Intuitionistic fuzzy logic and intuitionistic fuzzy set theory. J. Symbolic Logic, 49 (1984), 851–866.

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Technische UniversitätWien, Austria

    Matthias Baaz, Agata Ciabattoni & Christian G. Fermüller

Authors
  1. Matthias Baaz
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Agata Ciabattoni
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Christian G. Fermüller
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Software, Technical University of Catalonia, Jordi Girona 1, 08034, Barcelona, Spain

    Robert Nieuwenhuis

  2. Department of Computer Science, University of Manchester, Kilburn Building, Oxford Road, M13 9PL, Manchester, UK

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Baaz, M., Ciabattoni, A., Fermüller, C.G. (2001). Herbrand’s Theorem for Prenex Gödel Logic and Its Consequences for Theorem Proving. In: Nieuwenhuis, R., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2001. Lecture Notes in Computer Science(), vol 2250. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45653-8_14

Download citation

  • DOI: https://doi.org/10.1007/3-540-45653-8_14

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-42957-9

  • Online ISBN: 978-3-540-45653-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation