A Resolution Mechanism for Prenex Godel Logic

First order Godel logic G(infinity)(,)(Delta) enriched with the projection operator Delta-in contrast to other important t-norrn based fuzzy logics, like Lukasiewicz 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(infinity)(Delta) 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.