Combining second order matching and first order E-matching

Abstract : We propose an algorithm for combining second order matching and first order matching in an algebraic first order theory E. This algorithm has the flavor of the higher order E-unification algorithmof Nipkow and Qian, but relies on the classical second order matching algorithm of Huet and Lang instead of higher order unification. Since matching is simpler than unification, we are able to prove the termination of our algorithm when the algebraic theory E respects some conditions. We show that it is possible to preserve the termination when we relax some of these conditions by adapting the previous algorithm. It allows us to use AC1, ACI and ACI1 for example. These algebraic theories are the more useful for our purpose (recognizing logical or functional schemata). We have implemented our algorithm for the AC and AC1 theories and we show examples of possible applications.
Type de document :
Rapport
[Research Report] RR-2012, INRIA. 1993
Liste complète des métadonnées

https://hal.inria.fr/inria-00074659
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 16:01:16
Dernière modification le : samedi 17 septembre 2016 - 01:06:50
Document(s) archivé(s) le : mardi 12 avril 2011 - 18:07:46

Fichiers

Identifiants

  • HAL Id : inria-00074659, version 1

Collections

Citation

Régis Curien. Combining second order matching and first order E-matching. [Research Report] RR-2012, INRIA. 1993. 〈inria-00074659〉

Partager

Métriques

Consultations de la notice

184

Téléchargements de fichiers

42