Deutsch
 
Benutzerhandbuch Datenschutzhinweis Impressum Kontakt
  DetailsucheBrowse

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.


Zitierlink: http://hdl.handle.net/11858/00-001M-0000-000F-31E8-2
Zusammenfassung
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.