English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
 
 
DownloadE-Mail
  Proceedings of the 16th International Conference on Automated Deduction (CADE-16)

Ganzinger, H. (Ed.). (1999). Proceedings of the 16th International Conference on Automated Deduction (CADE-16). Berlin, Germany: Springer.

Item is

Files

show Files

Locators

show

Creators

show
hide
 Creators:
Ganzinger, Harald1, Editor           
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Content

show
hide
Free keywords: -
 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.

Details

show
hide
Language(s): eng - English
 Dates: 2010-03-121999
 Publication Status: Issued
 Pages: 443
 Publishing info: Berlin, Germany : Springer
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 519756
ISBN: 3-540-66222-7
Other: Local-ID: C1256104005ECAFC-9F8AF0350A7F2CFEC125688E00358D75-Ganzinger-ed-cade-1999
 Degree: -

Event

show
hide
Title: Untitled Event
Place of Event: Trento, Italy
Start-/End Date: 1999

Legal Case

show

Project information

show

Source 1

show
hide
Title: Lecture Notes in Artificial Intelligence
Source Genre: Series
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: 1632 Sequence Number: - Start / End Page: - Identifier: -