hide
Free keywords:
-
Abstract:
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.
