de.mpg.escidoc.pubman.appbase.FacesBean
English

Help Guide Disclaimer Contact us Login

# Item

ITEM ACTIONSEXPORT

Released

Conference Paper

#### On uniform word problems involving bridging operators on distributive lattices

##### MPS-Authors
http://pubman.mpdl.mpg.de/cone/persons/resource/persons45516

Sofronie-Stokkermans,  Viorica
Automation of Logic, MPI for Informatics, Max Planck Society;
Programming Logics, MPI for Informatics, Max Planck Society;

##### Locator
There are no locators available
##### Fulltext (public)
There are no public fulltexts available
##### Supplementary Material (public)
There is no public supplementary material available
##### Citation

Sofronie-Stokkermans, V. (2002). On uniform word problems involving bridging operators on distributive lattices. In Automated Reasoning with Analytic and Related Methods: International Conference, TABLEAUX 2002 (pp. 235-250). Berlin, Germany: Springer.

Cite as: http://hdl.handle.net/11858/00-001M-0000-000F-301F-0
##### Abstract
In this paper we analyze some fragments of the universal theory of distributive lattices with many sorted bridging operators. Our interest in such algebras is motivated by the fact that, in description logics, numerical features are often expressed by using maps that associate numerical values to sets (more generally, to lattice elements). We first establish a link between satisfiability of universal sentences with respect to algebraic models and satisfiability with respect to certain classes of relational structures. We use these results for giving a method for translation to clause form of universal sentences, and provide some decidability results based on the use of resolution or hyperresolution. Links between hyperresolution and tableau methods are also discussed, and a tableau procedure for checking satisfiability of formulae of type $t_1 \leq t_2$ is obtained by using a hyperresolution calculus.