de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch

Hilfe Wegweiser Impressum Kontakt Einloggen

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Zeitschriftenartikel

On unification for bounded distributive lattices

MPG-Autoren
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;

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

Sofronie-Stokkermans, V. (2007). On unification for bounded distributive lattices. ACM Transactions on Computational Logic, 8(2), 12.1-12.28. doi:10.1145/1227839.1227844.

We give a method for deciding unifiability in the variety of bounded distributive lattices. For this, we reduce the problem of deciding whether a unification problem ${\cal S}$ has a solution to the problem of checking the satisfiability of a set $\Phi_{\cal S}$ of ground clauses. This is achieved by using a structure-preserving translation to clause form. The satisfiability check can then be performed either by a resolution-based theorem prover or by a SAT checker. We apply the method to unification with free constants and to unification with linear constant restrictions, and show that, in fact, it yields a decision procedure for the positive theory of the variety of bounded distributive lattices. We also consider the problem of unification over (i.e.\ in an algebraic extension of) the free lattice. Complexity issues are also addressed.