On unification for bounded distributive lattices

ABSTRACT

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 S has a solution to the problem of checking the satisfiability of a set Φ_S of ground clauses. This is achieved by using a structure-preserving translation to clause form. The satisfiability check can then be performed by either a resolution-based theorem prover or 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.

REFERENCES

• 1: Franz Baader , Paliath Narendran, Unification of concept terms in description logics, Journal of Symbolic Computation, v.31 n.3, p.277-305, March 2001 [doi>10.1006/jsco.2000.0426 ]
• 2: Franz Baader , Klaus U. Schulz, Unification in the union of disjoint equational theories: combining decision procedures, Journal of Symbolic Computation, v.21 n.2, p.211-243, Feb. 1996 [doi>10.1006/jsco.1996.0009 ]
• 3: Franz Baader , Klaus U. Schulz, Combination of constraint solvers for free and quasi-free structures, Theoretical Computer Science, v.192 n.1, p.107-161, Feb. 10, 1998 [doi>10.1016/S0304-3975(97)00147-3 ]
• 4: Baader, F. and Snyder, W. 2001. Unification theory. In Handbook of Automated Reasoning, vol. 1, A. Robinson and A. Voronkov, eds. Elsevier Science. 445--532.
• 5: Birkhoff, G. 1933. On the combination of subalgebras. Proceedings of Cambridge Philosophical Society 29, 441--464.
• 6: Alexander Bockmayr, Model-Theoretic Aspects of Unification, Proceedings of the First International Workshop on Word Equations and Related Topics, p.181-196, October 01-03, 1990
• 7: Bürckert, H. 1991. A resolution principle for a logic with restricted quantifiers. Lecture Notes in Artificial Intelligence, vol. 568. Springer Verlag.
• 8: Burris, S. 1995. Polynomial time uniform word problems. Math. Logic Q. 41, 173--182.
• 9: Burris, S. and McKenzie, R. 1981. Decidability and Boolean representations. In Memoirs of the American Mathematical Society (series) vol. 32, 246. American Mathematical Society, Providence, RI.
• 10: Clark, D. M. and Davey, B. A. 1998. Natural dualities for the working algebraist. Cambridge Studies in Advanced Mathematics, vol. 57. Cambridge University Press, New York.
• 11: Davey, B. and Priestley, H. 1992. Introduction to lattices and order. Cambridge University Press, New York.
• 12: Dowling, W. and Gallier, J. 1984. Linear-Time algorithms for testing the satisfiability of propositional Horn formulae. J. Logic Program. 1, 3, 267--284.
• 13: Michael R. Garey , David S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman & Co., New York, NY, 1979
• 14: J. A. Gerhard , Mario Petrich, Unification in free distributive lattices, Theoretical Computer Science, v.126 n.2, p.237-257, April 25, 1994 [doi>10.1016/0304-3975(94)90011-6 ]
• 15: Ghilardi, S. 1997. Unification through projectivity. J. Logic Comput. 7, 6, 733--752.
• 16: Enrico Giunchiglia , Massimo Narizzano , Armando Tacchella, QUBE: A System for Deciding Quantified Boolean Formulas Satisfiability, Proceedings of the First International Joint Conference on Automated Reasoning, p.364-369, June 18-23, 2001
• 17: H. B. Hunt, III , D. J. Rosenkrantz , P. A. Bloniarz, On the computational complexity of algebra on lattices, SIAM Journal on Computing, v.16 n.1, p.129-148, Feb. 1987 [doi>10.1137/0216011]
• 18: H. B. Hunt , R. E. Stearns, The complexity of very simple Boolean formulas with applications, SIAM Journal on Computing, v.19 n.1, p.44-70, Feb. 1990 [doi>10.1137/0219003]
• 19: C. Kirchner , H. Kirchner, Constrained equational reasoning, Proceedings of the ACM-SIGSAM 1989 international symposium on Symbolic and algebraic computation, p.382-389, July 17-19, 1989, Portland, Oregon, United States [doi>10.1145/74540.74585]
• 20: Reinhold Letz, Lemma and Model Caching in Decision Procedures for Quantified Boolean Formulas, Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, p.160-175, July 30-August 01, 2002
• 21: McKinsey, J. 1943. The decision problem for some classes of sentences without quantifiers. The J. Symb. Logic 8, 3, 61--76.
• 22: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
• 23: Paliath Narendran, Unification modulo ACI + 1 + 0, Fundamenta Informaticae, v.25 n.1, p.48-57, Jan. 1996
• 24: Robert Nieuwenhuis , Albert Rubio, Theorem Proving with Ordering Constrained Clauses, Proceedings of the 11th International Conference on Automated Deduction: Automated Deduction, p.477-491, June 15-18, 1992
• 25: Priestley, H. 1972. Ordered topological spaces and the representation of distributive lattices. Proc. London Math. Soc. 3, 507--530.
• 26: Schmid, J. 1979. Algebraically and existentially closed distributive lattices. Zeitschrift für Math. Logik Grundlagen Inf. 25, 525--530.
• 27: Manfred Schmidt-Schauß, A decision algorithm for distributive unification, Theoretical Computer Science, v.208 n.1-2, p.111-148, Nov. 28, 1998 [doi>10.1016/S0304-3975(98)00081-4 ]
• 28: Viorica Sofronie-Stokkermans, On the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity Results, Proceedings of the 16th International Conference on Automated Deduction: Automated Deduction, p.157-171, July 07-10, 1999
• 29: Viorica Sofronie-Stokkermans, On Unification for Bonded Distributive Lattices, Proceedings of the 17th International Conference on Automated Deduction, p.465-481, June 17-20, 2000
• 30: Viorica Sofronie-Stokkermans, Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators, Journal of Symbolic Computation, v.36 n.6, p.891-924, December 2003 [doi>10.1016/S0747-7171(03)00069-5]
• 31: Resolution-Based Decision Procedures for the Positive Theory of Some Finitely Generated Varieties of Algebras, Proceedings of the 34th International Symposium on Multiple-Valued Logic (ISMVL'04), p.32-37, May 19-22, 2004
• 32: Christoph Weidenbach , Bernd Gaede , Georg Rock, SPASS & FLOTTER Version 0.42, Proceedings of the 13th International Conference on Automated Deduction: Automated Deduction, p.141-145, August 03, 1996

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic

Additional Classification:
  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.1 Expressions and Their Representation
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving

General Terms:
Algorithms, Theory

Keywords:
SAT solving, Theorem proving, decision procedures for the positive theory, distributive lattices, unification