Technical Foundations of a DPLL-Based SAT Solver for Propositional Gödel Logic

We provide the foundations of automated deduction in the propositional Gδdel logic. The propositional Gδdel logic is one of the simplest infinitely valued fuzzy logics, which generalizes classical propositional logic. We propose an extension of the Davis- Putnam-Logemann-Loveland (DPLL) procedure to this logic and prove its refutational soundness and finite completeness. Using the DPLL procedure, we solve the deduction problem T = φ (T is a finite theory and φ a formula), which covers the finite SAT problem for a theory and the VAL problem for a formula, obviously. This paper serves, on the one side, as a technical basis for the design of a SAT solver; on the other side, gives some preliminary theoretical results concerning the logical and computational foundations of fuzzy inference, which is our main aim.