Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:








Author, Editor

Author(s):

Sofronie-Stokkermans, Viorica

dblp



Editor(s):

Ganzinger, Harald

dblp



BibTeX cite key*:

Sofronie-Stokkermans1999-cade

Title, Booktitle

Title*:

On the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity Results


cade-99.pdf (248.45 KB)

Booktitle*:

Proceedings of the 16th International Conference on Automated Deduction (CADE-16)

Event, URLs

URL of the conference:

http://www.mpi-sb.mpg.de/cade-16/

URL for downloading the paper:


Event Address*:

Trento, Italy

Language:

English

Event Date*
(no longer used):

July 7-10, 1999

Organization:


Event Start Date:

22 October 2019

Event End Date:

22 October 2019

Publisher

Name*:

Springer

URL:


Address*:

Berlin, Germany

Type:


Vol, No, Year, pp.

Series:

Lecture Notes in Artificial Intelligence

Volume:

1632

Number:


Month:


Pages:

157-171

Year*:

1999

VG Wort Pages:


ISBN/ISSN:


Sequence Number:


DOI:




Note, Abstract, ©


(LaTeX) Abstract:

In this paper we give a method for automated theorem proving in the universal theory of certain varieties of distributive lattices with well-behaved operators. For this purpose, we use extensions of Priestley's representation theorem for distributive lattices. We first establish a link between satisfiability of universal sentences with respect to varieties of distributive lattices with operators and satisfiability with respect to certain classes of relational structures. We then use these results for giving a method for translation to clause form of universal sentences in such varieties, and obtain decidability and complexity results for the universal theory of some such varieties. The advantage is that we avoid the explicit use of the full algebraic structure of such lattices, instead using sets endowed with a reflexive and transitive relation and with additional functions and relations. We first studied this type of relationships in the context of finitely-valued logics and then extended the ideas to more

general non-classical logics. This paper shows that the idea is much more general. In particular, the method presented here subsumes both existing methods for translating modal logics to classical logic and methods for automated theorem proving in finitely-valued logics based on distributive lattices with operators.

URL for the Abstract:

http://link.springer.de/link/service/series/0558/bibs/1632/16320157.htm

Keywords:

Theorem Proving, Lattice Theory, Priestley Duality

HyperLinks / References / URLs:

http://link.springer.de/link/service/series/0558/bibs/1632/16320157.pdf

Copyright Message:

Copyright Springer


Download
Access Level:

Public

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:

@INPROCEEDINGS{Sofronie-Stokkermans1999-cade,
AUTHOR = {Sofronie-Stokkermans, Viorica},
EDITOR = {Ganzinger, Harald},
TITLE = {On the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity Results},
BOOKTITLE = {Proceedings of the 16th International Conference on Automated Deduction (CADE-16)},
PUBLISHER = {Springer},
YEAR = {1999},
VOLUME = {1632},
PAGES = {157--171},
SERIES = {Lecture Notes in Artificial Intelligence},
ADDRESS = {Trento, Italy},
}


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/01/1999 09:17:22 PM
Revisions
8.
7.
6.
5.
4.
Editor(s)
Viorica Sofronie-Stokkermans
Viorica Sofronie-Stokkermans
Viorica Sofronie-Stokkermans
Viorica Sofronie-Stokkermans
Viorica Sofronie-Stokkermans
Edit Dates
06/02/2003 11:42:03 AM
06/03/2000 13:58:11
27/05/99 11:07:44
25/05/99 21:18:52
25/05/99 21:17:29
Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section

View attachments here:


File Attachment Icon
cade-99.pdf