Proceedings Volume
@Proceedings
Tagungsband, Workshopband


Show entries of:

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

Action:

login to update

Options:








Author, Editor

Editor(s):

Ganzinger, Harald

dblp



BibTeX citekey*:

Ganzinger-ed-cade-1999

Language:

English

Title, Conference

Title*:

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



Event Address*:

Trento, Italy

Conference URL:

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

Event Start Date:

21 September 2019

Event End Date:

21 September 2019

Event Date*
(no longer used):

July 7-10, 1999

Organization:


Publisher

Name*:

Springer

Publisher's URL:






Address*:

Berlin, Germany

Publishing Year*:

1999

Vol, No, pp., Year

Series:

Lecture Notes in Artificial Intelligence

Volume:

1632

Number:


Month:


Pages*:

443

ISBN:

3-540-66222-7

VG Wort Pages:


ISSN:




Abstract, Links, ©

Note:


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.

Categories / Keywords:

Theorem Proving, Lattice Theory, Priestley Duality

HyperLinks / References / URLs:


Copyright Message:


Personal Comments:


Download
Access Level:


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:

@PROCEEDINGS{Ganzinger-ed-cade-1999,
EDITOR = {Ganzinger, Harald},
TITLE = {Proceedings of the 16th International Conference on Automated Deduction (CADE-16)},
PUBLISHER = {Springer},
YEAR = {1999},
VOLUME = {1632},
PAGES = {443},
SERIES = {Lecture Notes in Artificial Intelligence},
ADDRESS = {Trento, Italy},
ISBN = {3-540-66222-7},
}


Entry last modified by Manfred Jaeger, 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
02/23/2000 10:44:56 AM
Revisions
13.
12.
11.
10.
9.
Editor(s)
Manfred Jaeger
Christine Kiesel
Christine Kiesel
Christine Kiesel
Christine Kiesel
Edit Dates
27/08/2001 11:39:43
26.01.2001 03:08:24 PM
25.01.2001 04:04:07 PM
30/03/2000 16:15:20
23/02/2000 10:57:10