CONTEJEAN Evelyne
Ph.D
Group : Toccata
Elements for Decidability of Unification modulo Distributivity
Starts on 01/09/1988
Advisor :
Funding :
Affiliation : Université Paris-Saclay
Laboratory :
Defended on 03/04/1992, committee :
Gérard HUET, Président
Alain COLMERAUER
Mehmet DINCBAS
Marie-Claude GAUDEL
Jean-Pierre JOUANNAUD
Claude KIRCHNER
Leszec PACHOLSKI
Research activities :
- Automated deduction
- Rewriting
Abstract :
In this thesis, we give some tools for unification (or equations solving) modulo distributivity (or modulo D) of a symbol f on a symbol g. This theory is one of the last for which it remains still unkown whether it is decidable or not.
In the first part, we study some particular problems obviously decidable, balanced problems containing only some terms without the g symbol. We precisely describe the set of solutions, which is possibly infinite. This is done with structures for which there is a property of unique maximal decomposition with respect to a AC1 operator. In a second part, the notions of indexation and stratification are introduced and are used in order to characterize the equality modulo D of two terms. Then we prove, thanks to stratification, the completeness of a set of transformation rules. This set reduces a problem to a babanced problem, and a balanced problem is solved by AC1 unification on structures. For technical reasons, we only handle a particular sort of problems, caracterized by a condition of acyclicity.
Finally, we describe a new, efficient algorithm for solving systems of linear Diophantine equations.