English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Journal Article

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

MPS-Authors
/persons/resource/persons45516

Sofronie-Stokkermans,  Viorica
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
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.