On the Satisfiability and Validity Problems in the Propositional Gödel Logic

Abstract

This paper addresses the satisfiability and validity problems of a formula in the propositional Gödel logic. Our approach is based on the translation of a formula to an equivalent CNF one which contains literals of the augmented form: either a or a → b or (a → b) → b, where a, b are propositional atoms or the propositional constants 0, 1. Since the equivalent output CNF may be exponential in the size of an input formula, we improve the translation using interpolation rules so that output CNF formulae are in linear size with respect to input ones; however, not equivalent - only equisatisfiable. A CNF formula is further translated to an equisatisfiable finite order clausal theory which consists of order clauses - finite sets of order literals of the forms $a\eqcirc b$ or a ≺ b, where $\eqcirc$ and ≺ are interpreted by the equality and strict linear order on [0,1], respectively. A variant of the DPLL procedure, operating on order clausal theories, is proposed. The DPLL procedure is proved to be refutation sound and complete for countable order clausal theories. Finally, the validity problem of a formula (tautology checking) is reduced to the unsatisfiability of a finite order clausal theory.

Partially supported by the grants VEGA 1/0688/10, VEGA 1/0726/09, and Slovak Literary Fund.