Skip to Main content Skip to Navigation

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.
Document type :
Complete list of metadata
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 4:01:16 PM
Last modification on : Thursday, February 11, 2021 - 2:48:31 PM
Long-term archiving on: : Tuesday, April 12, 2011 - 6:07:46 PM


  • HAL Id : inria-00074659, version 1



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



Record views


Files downloads