Third order matching is decidable

DOI10.1016/0168-0072(94)90083-3MaRDI QIDQ1337691zbMATH OpenOpenAlexFDO

Authors Gilles Dowek

Publication date 8 November 1994

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0168-0072(94)90083-3

zbMATH Keywords

interpolationdecidabilitythird ordermatching problemsimply typed \(\lambda\)-calculus

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Combinatory logic and lambda calculus (03B40)

Recommendations

• Third-order matching in the polymorphic lambda calculus
• scientific article; zbMATH DE number 2185677
• Higher Order   Matching is Undecidable
• Computer Science Logic
• Decidability of fourth-order matching

Cites work

• scientific article; zbMATH DE number 3935004 (Why is no real title available?)
• scientific article; zbMATH DE number 3993540 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• A unification algorithm for typed -calculus
• Completeness, invariance and λ-definability
• Higher-order unification revisited: Complete sets of transformations
• Proving and applying program transformations expressed with second-order patterns
• The Clausal Theory of Types
• The lambda calculus, its syntax and semantics
• Unification under a mixed prefix

Cited in

(16)

• A colored version of the \(\lambda\)-calculus
• Third-order matching in the polymorphic lambda calculus
• Decidability of all minimal models
• The variable containment problem
• scientific article; zbMATH DE number 2185677 (Why is no real title available?)
• On the undecidability of second-order unification
• Unification for \(\lambda\)-calculi without propagation rules
• Higher Order   Matching is Undecidable
• Nominal syntax with atom substitutions
• Decidability of bounded higher-order unification
• Higher-order beta matching with solutions in long beta-eta normal form
• Fundamentals of Computation Theory
• Decidable higher-order unification problems
• Typed answer set programming lambda calculus theories and correctness of inverse lambda algorithms with respect to them
• The inverse lambda calculus algorithm for typed first order logic lambda calculus and its application to translating English to FOL
• Model-checking games for typed \(\lambda\)-calculi

This page was built for publication: Third order matching is decidable

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1337691)