A DPLL PROCEDURE FOR THE PROPOSITIONAL GODEL LOGIC

摘要

In the paper, we investigate the satisfiability and validity problems of a formula in the propositional Godel 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. 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 = b or a < b. = and < are interpreted by the equality and strict linear order on [0,1], respectively. A variant of the DPLL procedure for deciding the satisfiability of a finite order clausal theory is proposed. The DPLL procedure is proved to be refutation sound and complete. Finally, we reduce the validity problem of a formula (tautology checking) to the unsatisfiability of a finite order clausal theory.