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 (restricted access)
There are currently no full texts shared for your IP range.
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: https://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.