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 \(\mathcal{S}\) to the problem of checking the satisfiability of a set Φ 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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Baader, F.: On the complexity of Boolean unification. Information Processing Letters 67(4), 215–220 (1998)
Baader, F., Narendran, P.: Unification of concept terms in description logics. In: Prade, H. (ed.) Proceedings of ECAI 1998, pp. 331–335. Wiley, Chichester (1998)
Baader, F., Schulz, K.U.: Unification in the union of disjoint equational theories: Combining decision procedures. J. Symbolic Computation 21, 211–243 (1996)
Baader, F., Schulz, K.U.: Combination of constraint solvers for free and quasifree structures. Theoretical Computer Science 192, 107–161 (1998)
Baader, F., Snyder, W.: Unification theory. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning. Elsevier, Amsterdam (2000) (to appear)
Bachmair, L., Ganzinger, H., Waldmann, U.: Set constraints are the monadic class. In: Eighth Annual IEEE Symposium on Logic in Computer Science, Montreal, Canada, June 19-23, pp. 75–83. IEEE Computer Society Press, Los Alamitos (1993)
Bockmayr, A.: Algebraic and logical aspects of unification. In: Schulz, K.U. (ed.) IWWERT 1990. LNCS, vol. 572, pp. 171–180. Springer, Heidelberg (1992)
Bockmayr, A.: Model-theoretic aspects of unification. In: Schulz, K.U. (ed.) IWWERT 1990. LNCS, vol. 572, pp. 181–196. Springer, Heidelberg (1992)
Bürckert, H.J.: A Resolution Principle for a Logic with Restricted Quantifiers. LNCS (LNAI), vol. 568. Springer, Heidelberg (1991)
Burris, S., Sankappanavar, H.P.: A Course in Universal Algebra. In: Graduate Texts in Mathematics. Springer, Heidelberg (1981)
Dowling, W.F., Gallier, J.H.: Linear-time algorithms for testing the satisfiability of propositional Horn formulae. J. Logic Programming 1(3), 267–284 (1984)
Gerhard, J.A., Petrich, M.: Unification in free distributive lattices. Theoretical Computer Science 126(2), 237–257 (1994)
Ghilardi, S.: Unification through projectivity. J. Logic and Computation 7(6), 733–752 (1997)
Hunt, H.B., Rosenkrantz, D.J., Bloniarz, P.A.: On the computational complexity of algebra of lattices. SIAM Journal of Computation 16(1), 129–148 (1987)
Hunt, H.B., Stearns, R.E.: The complexity of very simple Boolean formulas with applications. SIAM J. Comput. 19(1), 44–70 (1990)
Kirchner, C., Kirchner, H.: Constrained equational reasoning. In: UNIF 1989 Extended Abstacts of the 3rd Int. Workshop on Unification, Pfalzakademie, Lambrecht, pp. 160–171 (1989)
Nieuwenhuis, R., Rubio, A.: Theorem proving with ordering constrained clauses. In: Kapur, D. (ed.) CADE 1992. LNCS (LNAI), vol. 607, pp. 477–491. Springer, Heidelberg (1992)
Priestley, H.A.: Ordered topological spaces and the representation of distributive lattices. Proc. London Math. Soc. 3, 507–530 (1972)
Schmidt-Schauß, M.: A decision algorithm for distributive unification. Theoretical Computer Science 208(1–2), 111–148 (1998)
Sofronie-Stokkermans, V.: On the universal theory of varieties of distributive lattices with operators: Some decidability and complexity results. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 157–171. Springer, Heidelberg (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sofronie-Stokkermans, V. (2000). On Unification for Bounded Distributive Lattices. In: McAllester, D. (eds) Automated Deduction - CADE-17. CADE 2000. Lecture Notes in Computer Science(), vol 1831. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10721959_38
Download citation
DOI: https://doi.org/10.1007/10721959_38
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67664-5
Online ISBN: 978-3-540-45101-3
eBook Packages: Springer Book Archive