English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
Add to Basket
 Local TagsRelease HistoryDetailsSummary
  On the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity Results

Sofronie-Stokkermans, V. (1999). On the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity Results. In H. Ganzinger (Ed.), Proceedings of the 16th International Conference on Automated Deduction (CADE-16) (pp. 157-171). Berlin, Germany: Springer.

Item is

 

show all hide all

Basic

show hide
Item Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-367B-0 Version Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-367D-C
Genre: Conference Paper

Files

show Files

Locators

show

Creators

show
hide
 Creators:
Sofronie-Stokkermans, Viorica1, 2, Author           
Affiliations:
1Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              
2Programming 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: -
 Publishing info: -
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 519864
Other: Local-ID: C1256104005ECAFC-377126A3548F6E6CC12567460069F5E0-Sofronie-Stokkermans1999-cade
 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: Proceedings of the 16th International Conference on Automated Deduction (CADE-16)
Source Genre: Proceedings
 Creator(s):
Ganzinger, Harald1, Editor           
Affiliations:
1 Programming Logics, MPI for Informatics, Max Planck Society, ou_40045            
Publ. Info: Berlin, Germany : Springer
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 157 - 171 Identifier: -

Source 2

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: -