Third order matching is decidable

Annals of Pure and Applied Logic 69 (2-3):135-155 (1994)
  Copy   BIBTEX

Abstract

The higher order matching problem is the problem of determining whether a term is an instance of another in the simply typed [lgr]-calculus, i.e. to solve the equation a = b where a and b are simply typed [lgr]-terms and b is ground. The decidability of this problem is still open. We prove the decidability of the particular case in which the variables occuring in the problem are at most third order

Categories

Keywords

Reprint years

DOI

10.1016/0168-0072(94)90083-3

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 92,323

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

An Undecidable Linear Order That Is $n$-Decidable for All $n$.John Chisholm & Michael Moses - 1998 - Notre Dame Journal of Formal Logic 39 (4):519-526.
On countable chains having decidable monadic theory.Alexis Bés & Alexander Rabinovich - 2012 - Journal of Symbolic Logic 77 (2):593-608.
The theory of integer multiplication with order restricted to primes is decidable.Françoise Maurin - 1997 - Journal of Symbolic Logic 62 (1):123-130.
Pure Second-Order Logic with Second-Order Identity.Alexander Paseau - 2010 - Notre Dame Journal of Formal Logic 51 (3):351-360.
Periodicity Based Decidable Classes in a First Order Timed Logic.Danièle Beauquier & Anatol Slissenko - 2006 - Annals of Pure and Applied Logic 139 (1):43-73.
On a decidable generalized quantifier logic corresponding to a decidable fragment of first-order logic.Natasha Alechina - 1995 - Journal of Logic, Language and Information 4 (3):177-189.
Decidable discrete linear orders.M. Moses - 1988 - Journal of Symbolic Logic 53 (2):531-539.
Unification grammars and off-line parsability.Efrat Jaeger, Nissim Francez & Shuly Wintner - 2005 - Journal of Logic, Language and Information 14 (2):199-234.
Decidable subspaces and recursively enumerable subspaces.C. J. Ash & R. G. Downey - 1984 - Journal of Symbolic Logic 49 (4):1137-1145.
A decidable variety that is finitely undecidable.Joohee Jeong - 1999 - Journal of Symbolic Logic 64 (2):651-677.
An Event-Based Fragment of First-Order Logic over Intervals.Savas Konur - 2011 - Journal of Logic, Language and Information 20 (1):49-68.
First-order and counting theories of ω-automatic structures.Dietrich Kuske & Markus Lohrey - 2008 - Journal of Symbolic Logic 73 (1):129-150.
On first-order theories with provability operator.Sergei Artëmov & Franco Montagna - 1994 - Journal of Symbolic Logic 59 (4):1139-1153.
Decidable fragments of first-order modal logics.Frank Wolter & Michael Zakharyaschev - 2001 - Journal of Symbolic Logic 66 (3):1415-1438.
Automatic structures of bounded degree revisited.Dietrich Kuske & Markus Lohrey - 2011 - Journal of Symbolic Logic 76 (4):1352-1380.

Analytics

Added to PP
2014-01-16

Downloads
11 (#1,143,314)

6 months
5 (#648,315)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Typed lambda calculus.Henk P. Barendregt, Wil Dekkers & Richard Statman - 1977 - In Jon Barwise (ed.), Handbook of mathematical logic. New York: North-Holland. pp. 1091--1132.
Higher order unification and the interpretation of focus.Stephen G. Pulman - 1997 - Linguistics and Philosophy 20 (1):73-115.

Add more citations

References found in this work

Completeness, invariance and λ-definability.R. Statman - 1982 - Journal of Symbolic Logic 47 (1):17-26.
The Clausal Theory of Types.D. A. Wolfram - 1993 - Cambridge University Press.

Add more references