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 λσ-style of explicit substitutions. We introduce a convenient notation for matching in the λσ-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.
Keywords Higher-Order Unification - Second-Order Matching - Explicit Substitutions
Work supported by funds from CNPq(CT-INFO) 50.6598/04-7 and PRONEX.