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
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
A. Avron. Hypersequents, Logical Consequence and Intermediate Logics for Concurrency. Annals of Mathematics and Artificial Intelligence Vol. 4, 1991, 225–248.
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.
F. Baader, T. Nipkow. Term Rewriting and All That. Cambridge UP, 1998.
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.
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
M. Baaz, U. Egly, A. Leitsch. Normal Form Transformations. Handbook of Automated Reasoning 1 Eds: A. Robinson, A. Voronkov. Elsevier, 2001, 273–333.
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.
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.
M. Baaz, H. Veith. Quantifier Elimination in Fuzzy Logic. Computer Science Logic, 12th International Workshop, CSL’98, LNCS 1584, 1999, 399–414.
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.
M. Baaz, H. Veith. Interpolation in fuzzy logic. Arch. Math. Logic, 38 (1999), 461–489.
M. Baaz, R. Zach. Hypersequents and the Proof Theory of Intuitionistic Fuzzy Logic. Proc. CSL’2000, 2000, 187–201.
L. Bachmair, H. Ganzinger. Ordered Chaining forTotal Orderings. Proc. CADE’94, Springer LNCS 814, 1994, 435–450.
L. Bachmair, H. Ganzinger. Ordered Chaining Calculi for First-Order Theories of Transitive Relations. J. ACM 45(6) (1998), 1007–1049.
A. Degtyarev, A. Voronkov. Decidability Problems for the Prenex Fragment of Intuitionistic Logic. In Proceedings LICS’96. IEEE Press, 503–509. 1996.
M. Dummett. A propositional calculus with denumerable matrix. J. Symbolic Logic, 24(1959), 97–106.
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.
R. Dyckhoff. A Deterministic Terminating Sequent Calculus for Gödel-Dummett Logic. Logic Journal of the IGPL, 7(1999), 319–326.
D.M. Gabbay. Decidability of some intuitionistic predicate theories. J. of Symbolic Logic, vol. 37, pp. 579–587. 1972.
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.
P. Hájek. Metamathematics of Fuzzy Logic. Kluwer, 1998.
A. Horn. Logic with truth values in a linearly ordered Heyting algebra. J. Symbolic Logic, 27 (1962), 159–170.
A. Leitsch. The Resolution Calculus. Springer, 1997. Kluwer, 1998.
D. Plaisted, S. Greenbaum. A Structure-Preserving Clause Form Translation. J. Symbolic Computation 2 (1986), 293–304.
H. Rogers. Certain logical reduction and decision problems. Annals of Mathematics, vol. 64, pp. 264284. 1956.
G. Takeuti, T. Titani. Intuitionistic fuzzy logic and intuitionistic fuzzy set theory. J. Symbolic Logic, 49 (1984), 851–866.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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