# Item

ITEM ACTIONSEXPORT

Released

Journal Article

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

##### Fulltext (public)

There are no public fulltexts stored in PuRe

##### Supplementary Material (public)

There is no public supplementary material available

##### Citation

Sofronie-Stokkermans, V. (2001). Automated Theorem Proving by Resolution for Finitely-Valued
Logics Based on Distributive Lattices with Operators.* Multiple-Valued Logic - An International Journal,*
*6*(3/4), 289-344.

Cite as: http://hdl.handle.net/11858/00-001M-0000-000F-31E8-2

##### 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.