Second-order matching via explicit substitutions

F. L C De Moura, Fairouz Kamareddine, Mauricio Ayala-Rincón

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages433-448
Number of pages16
Volume3452 LNAI
Publication statusPublished - 2005
Event11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning - Montevideo, Uruguay
Duration: 14 Mar 200518 Mar 2005

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3452 LNAI
ISSN (Print)0302-9743

Conference

Conference11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning
Abbreviated titleLPAR 2004
CountryUruguay
CityMontevideo
Period14/03/0518/03/05

Keywords

  • Explicit Substitutions
  • Higher-Order Unification
  • Second-Order Matching

Fingerprint Dive into the research topics of 'Second-order matching via explicit substitutions'. Together they form a unique fingerprint.

  • Cite this

    De Moura, F. L. C., Kamareddine, F., & Ayala-Rincón, M. (2005). Second-order matching via explicit substitutions. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3452 LNAI, pp. 433-448). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3452 LNAI).