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

Proceedings Volume
@Proceedings
Tagungsband, Workshopband

Show entries of:

this year (2024) | last year (2023) | two years ago (2022) | Notes URL

Action:

Options:

Goto entry point

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:	15 May 2024	Event End Date:	15 May 2024
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:

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

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