Theorem proving for prenex Gödel logic with : checking validity and unsatisfiability

DOI10.2168/LMCS-8(1:20)2012MaRDI QIDQ2881087zbMATH OpenOpenAlexFDO

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

Publication date 3 April 2012

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1202.6352

zbMATH Keywords

\(\Delta\) modalitychaining calculusfuzzy logicGödel logicHerbrand's theoremresolutionSkolemizationtheorem proving

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Many-valued logic (03B50) Fuzzy logic; logic of vagueness (03B52)

Abstract: G"odel logic with the projection operator Delta (G_Delta) is an important many-valued as well as intermediate logic. In contrast to classical logic, the validity and the satisfiability problems of G_Delta are not directly dual to each other. We nevertheless provide a uniform, computational treatment of both problems for prenex formulas by describing appropriate translations into sets of order clauses that can be subjected to chaining resolution. For validity a version of Herbrand's Theorem allows us to show the soundness of standard Skolemization. For satisfiability the translation involves a novel, extended Skolemization method.

Recommendations

• A resolution mechanism for prenex Gödel logic
• Herbrand's theorem for prenex Gödel logic and its consequences for theorem proving
• Unsatisfiable Formulae of Gödel Logic with Truth Constants and $$\varDelta $$ Are Recursively Enumerable
• Automated deduction in Gödel logic
• Gödel logics with monotone operators

Cited in

(5)

• Hyperresolution for Gödel logic with truth constants
• Herbrand's theorem for prenex Gödel logic and its consequences for theorem proving
• A resolution mechanism for prenex Gödel logic
• Theorem proving for conditional logics: CondLean and GOALDUCK
• Unsatisfiable Formulae of Gödel Logic with Truth Constants and $$\varDelta $$ Are Recursively Enumerable

This page was built for publication: Theorem proving for prenex Gödel logic with \(\Delta\): checking validity and unsatisfiability

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2881087)