Journal Article @Article Artikel in Fachzeitschrift
 Show entries of: this year (2019) | last year (2018) | two years ago (2017) | Notes URL
 Action: login to update Options: Goto entry point

 Author, Editor(s)
 Author(s): Sofronie-Stokkermans, Viorica dblp
 BibTeX cite key*: Sofronie-Stokkermans1999

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

 Journal
 Journal Title*: Multiple-Valued Logic - An International Journal Journal's URL: http://taylorandfrancis.metapress.com/openurl.asp?genre=journal&issn=1023-6627 Download URL for the article: Language: English

 Publisher
 Publisher's Name: Gordon and Breach Publisher's URL: http://taylorandfrancis.metapress.com/ Publisher's Address: Amsterdam, the Netherlands ISSN: 1023-6627

 Vol, No, pp, Date
 Volume*: 6 Number: 3/4 Publishing Date: March 2001 Pages*: 289-344 Number of VG Pages: Page Start: Page End: Sequence Number: DOI:

 Note: (LaTeX) 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. URL for the Abstract: http://www.mpi-sb.mpg.de/~sofronie/abstracts.html#logic-fv Categories, Keywords: HyperLinks / References / URLs: Copyright Message: Copyright Gordon and Breach Personal Comments: Download Access Level: Intranet

 Correlation
 MPG Unit: Max-Planck-Institut für Informatik MPG Subunit: Programming Logics Group Audience: experts only Appearance: MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat

BibTeX Entry:

@ARTICLE{Sofronie-Stokkermans1999,
AUTHOR = {Sofronie-Stokkermans, Viorica},
TITLE = {Automated Theorem Proving by Resolution for Finitely-Valued Logics Based on Distributive Lattices with Operators},
JOURNAL = {Multiple-Valued Logic - An International Journal},
PUBLISHER = {Gordon and Breach},
YEAR = {2001},
NUMBER = {3/4},
VOLUME = {6},
PAGES = {289--344},