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

# Item

ITEM ACTIONSEXPORT

Released

Conference Paper

#### On unification for bounded 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. (2000). On unification for bounded distributive lattices. In D. McAllester (), Proceedings of the 17th International Conference on Automated Deduction (CADE-17) (pp. 465-481). Berlin, Germany: Springer.

Cite as: http://hdl.handle.net/11858/00-001M-0000-000F-3450-D
##### Abstract
We give a resolution-based procedure for deciding unifiability in the variety of bounded distributive lattices. The main idea is to use a structure-preserving translation to clause form to reduce the problem of testing the satisfiability of a unification problem ${\cal S}$ to the problem of checking the satisfiability of a set $\Phi_{\cal S}$ of (constrained) clauses. These ideas can be used for unification with free constants and for unification with linear constant restrictions. Complexity issues are also addressed.