Deduction and Unification in Permutative Theories

Relatore
Dr. Mnacho Echenim - Institut National Polytechnique de Grenoble

Data e ora
martedì 21 febbraio 2006 alle ore 17.30 - caffè, tè & C. ore 17.00

Luogo
Ca' Vignal 3 - Piramide, Piano 0, Sala Verde

Referente
Maria Paola Bonacina

Referente esterno

Data pubblicazione
9 febbraio 2006

Dipartimento
 

Riassunto

Many state-of-the art theorem provers can perform deductions modulo an equational theory, by considering equivalence classes of terms, instead of ordinary terms. Most of the existing approaches focus on determining new and more efficient techniques to perform deduction modulo only one theory, such as associativity and commutativity. A more general research direction is to try to determine efficient techniques that could be used to treat not one specific theory, but an entire class of equational theories. If such techniques were to be integrated in a theorem prover, it would be possible to solve several problems very efficiently without any prior human intervention.

In this presentation, we will consider the class of leaf-permutative theories. These theories enjoy several regularity properties that make it possible to use efficient techniques from computational group theory to deal with them. The use of group-theoretic techniques is nontrivial, and I will show that it can be done quite elegantly thanks to the conceps of stratified term-graphs. There are several problems any theorem prover dealing with leaf-permutative theories has to solve, and thanks to our formalism, we can prove that these problems are all NP-hard. Finally, I will present a subclass of leaf-permutative theories, the so-called unify-stable theories, that enjoy better complexity properties, and I will show that we can solve any unification problem modulo such a theory.
ornamento
Inizio pagina