LIBRARY OF UNIFICATION ALGORITHMS ================================= The goal of this project is to develop a Prolog library of unification algorithms in various theories. The project consists of several subprojects. Within each subproject, unification algorithm for a particular theory is implemented by a small group of students (2-4 members). The current list of subprojects are: --------------------------------------- 1. ASSOCIATIVE-COMMUTATIVE UNIFICATION --------------------------------------- Literature: Alexandre Boudet, Evelyne Contejean, and Hervé Devie. A new AC-unification algorithm with a new algorithm for solving diophantine equations. In Proc. 5th IEEE Symp. Logic in Computer Science, Philadelphia, pages 289-299. IEEE Computer Society Press, June 1990. Farid Ajili and Evelyne Contejean. Avoiding slack variables in the solving of linear diophantine equations and inequations. Theoretical Computer Science, 173(1):183-208, February 1997. Evelyne Contejean and Hervé Devie. An efficient algorithm for solving systems of diophantine equations. Information and Computation, 113(1):143-172, August 1994. --------------------------------------- 2. UNIFICATION OF HIGHER-ORDER PATTERNS --------------------------------------- Literature: Tobias Nipkow. Functional unification of higher-order patterns. In Eighth Annual IEEE Symposium on Logic in Computer Science, pages 64–74. IEEE Computer Society Press, June 1993. ---------------------------------- 3. LINEAR SECOND-ORDER UNIFICATION ---------------------------------- Literature: Jordi Levy. Linear Second Order Unification. Proc. of the 7th International Conference on Rewriting Techniques and Applications, RTA'96. Lecture Notes in Computer Science, Vol. 1103, pp. 332-346. Springer-Verlag, 1996. Mateu Villaret. On Some Variants of Second-Order Unification. PhD. Thesis. Universitat Politecnica de Catalunya. 2004. ----------------------- 4. SEQUENCE UNIFICATION ----------------------- Literature: Temur Kutsia. Solving Equations with Sequence Variables and Sequence Functions. J. Symbolic Computation, 42(3):352--388, 2007. ------------------------------- 5. UNIFICATION IN BOOLEAN RINGS ------------------------------- Literature: Ursula Martin, Tobias Nipkow: Unification in Boolean Rings. J. Autom. Reasoning 4(4): 381-396. 1988.