TY - GEN
T1 - Second-order matching via explicit substitutions
AU - De Moura, F. L C
AU - Kamareddine, Fairouz
AU - Ayala-Rincón, Mauricio
PY - 2005
Y1 - 2005
N2 - Matching is a basic operation extensively used in computation. Second-order matching, in particular, provides an adequate environment for expressing program transformations and pattern recognition for automated deduction. The past few years have established the benefit of using explicit substitutions for theorem proving and higher-order unification. In this paper, we will make use of explicit substitutions to facilitate matching: we develop a second-order matching algorithm via the ?s-style of explicit substitutions. We introduce a convenient notation for matching in the ?s-calculus. This notation keeps the matching equations separated from the incremental graftings. We characterise an important class of second-order matching problems which is essential to prove termination of the algorithm. In addition, we illustrate how the algorithm works through some examples. © Springer-Verlag Berlin Heidelberg 2005.
AB - Matching is a basic operation extensively used in computation. Second-order matching, in particular, provides an adequate environment for expressing program transformations and pattern recognition for automated deduction. The past few years have established the benefit of using explicit substitutions for theorem proving and higher-order unification. In this paper, we will make use of explicit substitutions to facilitate matching: we develop a second-order matching algorithm via the ?s-style of explicit substitutions. We introduce a convenient notation for matching in the ?s-calculus. This notation keeps the matching equations separated from the incremental graftings. We characterise an important class of second-order matching problems which is essential to prove termination of the algorithm. In addition, we illustrate how the algorithm works through some examples. © Springer-Verlag Berlin Heidelberg 2005.
KW - Explicit Substitutions
KW - Higher-Order Unification
KW - Second-Order Matching
UR - http://www.scopus.com/inward/record.url?scp=26844490183&partnerID=8YFLogxK
M3 - Conference contribution
SN - 3540252363
SN - 9783540252368
VL - 3452 LNAI
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 433
EP - 448
BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
T2 - 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning
Y2 - 14 March 2005 through 18 March 2005
ER -