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

DOI10.1007/3-540-45653-8_14zbMath1275.03098MaRDI QIDQ2996163

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

Publication date: 6 May 2011

Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-45653-8_14

Mathematics Subject Classification ID

03B35: Mechanization of proofs and logical operations

03B50: Many-valued logic

Related Items

The eskolemization of universal quantifiers, A first order nonmonotonic extension of constructive logic, Arithmetical complexity of fuzzy predicate logics -- a survey, On the refutational completeness of signed binary resolution and hyperresolution, Ten problems in Gödel logic, The Skolemization of prenex formulas in intermediate logics, On the predicate logics of continuous t-norm BL-algebras, A proof-theoretical investigation of global intuitionistic (fuzzy) logic, Triangular norm based predicate fuzzy logics, Hyperresolution for Gödel logic with truth constants, First-order Gödel logics, Automated theorem proving by resolution in non-classical logics, A Generalisation of the Hyperresolution Principle to First Order Gödel Logic, Monadic Fragments of Gödel Logics: Decidability and Undecidability Results, Herbrand Theorems and Skolemization for Prenex Fuzzy Logics, SAT in Monadic Gödel Logics: A Borderline between Decidability and Undecidability