Deutsch

Benutzerhandbuch Datenschutzhinweis Impressum Kontakt

# Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Zeitschriftenartikel

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

##### MPG-Autoren
/persons/resource/persons45516

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

##### Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
##### Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte verfügbar
##### Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
##### Zitation

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.

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.