A Resolution Mechanism for Prenex Gödel Logic

Abstract

First order Gödel logic G$^\Delta_\infty$, enriched with the projection operator Δ—in contrast to other important t-norm based fuzzy logics, like Łukasiewicz and Product logic—is well known to be recursively axiomatizable. However, unlike in classical logic, testing (1-)unsatisfiability, i.e., checking whether a formula has no interpretation that assigns the designated truth value 1 to it, cannot be straightforwardly reduced to testing validity. We investigate the prenex fragment of G$^\Delta_\infty$ and show that, although standard Skolemization does not preserve 1-satisfiability, a specific Skolem form for satisfiability can be computed nevertheless. In a further step an efficient translation to a particular structural clause form is introduced. Finally, an adaption of a chaining calculus is shown to provide a basis for efficient, resolution style theorem proving.