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:








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, Abstract, ©

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},
ADDRESS = {Amsterdam, the Netherlands},
MONTH = {March},
ISBN = {1023-6627},
}


Entry last modified by Viorica Sofronie-Stokkermans, 03/12/2010
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Viorica Sofronie-Stokkermans
Created
04/13/1999 11:37:26 AM
Revisions
16.
15.
14.
13.
12.
Editor(s)
Viorica Sofronie-Stokkermans
Viorica Sofronie-Stokkermans
Uwe Brahm
Viorica Sofronie-Stokkermans
Viorica Sofronie-Stokkermans
Edit Dates
05/23/2003 03:44:21 PM
05/23/2003 03:42:54 PM
04.04.2002 02:26:08
16/01/2002 10:15:39
05.09.2001 16:35:22