Automated Theorem Proving by Resolution for Finitely-Valued Logics Based on Distributive Lattices with Operators

In this paper we present a method for automated theorem proving in finitely-valued logics whose algebra of truth values is a distributive lattice with operators. The method uses the Priestley dual of the algebra of truth values instead of the algebra itself (this dual is used as a finite set of possible worlds). We first present a procedure that constructs, for every formula $\phi$ in the language of such a logic, a set $\Phi$ of clauses such that $\phi$ is a theorem if and only if $\Phi$ is unsatisfiable. Compared to related approaches, the method presented here leads in many cases to a reduction of the number of clauses that are generated, especially when the set of truth values is not linearly ordered. We then discuss several possibilities for checking the unsatisfiability of $\Phi$, among which a version of signed hyperresolution, and give several examples