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.