zbMATH — the first resource for mathematics

Herbrand’s theorem for prenex Gödel logic and its consequences for theorem proving. (English) Zbl 1275.03098
Nieuwenhuis, Robert (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 8th international conference, LPAR 2001, Havana, Cuba, December 3–7, 2001. Proceedings. Berlin: Springer (ISBN 3-540-42957-3/pbk). Lecture Notes in Computer Science 2250. Lecture Notes in Artificial Intelligence, 201-216 (2001).
Summary: Herbrand’s theorem for G\(_{\infty } ^{\Delta }\) , i.e., Gödel logic enriched by the projection operator \(\Delta \), is proved. As a consequence we obtain a “chain normal form” and a translation of prenex G\(_{\infty } ^{\Delta }\) 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.
For the entire collection see [Zbl 1046.03001].

03B50 Many-valued logic
03B35 Mechanization of proofs and logical operations
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI