A decidable variant of higher order matching

DOI10.1007/3-540-45610-4_24MaRDI QIDQ4808757zbMATH OpenFDO

Authors Tomasz Wierzbicki, Daniel J. Dougherty

Publication date 12 August 2004

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2378/23780340.htm

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Grammars and rewriting systems (68Q42)

Recommendations

• Higher-order matching in the linear -calculus with pairing
• Linear higher-order matching is NP-complete
• Higher-order beta matching with solutions in long beta-eta normal form
• Decidability of fourth-order matching
• Higher Order   Matching is Undecidable

Cited in

(10)

• Decidability of bounded higher-order unification
• Computing interpolants in implicational logics
• Linear higher-order matching is NP-complete
• On the complexity of higher-order matching in the linear -calculus
• The variable containment problem
• Higher Order   Matching is Undecidable
• Higher-order matching in the linear -calculus with pairing
• Fundamentals of Computation Theory
• Higher-order matching in the linear lambda calculus in the absence of constants is NP-complete
• Automated Deduction – CADE-19

This page was built for publication: A decidable variant of higher order matching

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