Higher-order beta matching with solutions in long beta-eta normal form

MaRDI QIDQ3431410zbMATH OpenFDO

Authors Kristian Støvring

Publication date 10 April 2007

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)

Recommendations

• Higher Order   Matching is Undecidable
• Third order matching is decidable
• Decidability of fourth-order matching
• Automated Deduction – CADE-19
• scientific article; zbMATH DE number 1223619

Cited in

(9)

• scientific article; zbMATH DE number 2185677 (Why is no real title available?)
• Dependency Tree Automata
• scientific article; zbMATH DE number 1223619 (Why is no real title available?)
• Decidability of fourth-order matching
• Higher Order   Matching is Undecidable
• scientific article; zbMATH DE number 2090083 (Why is no real title available?)
• Higher order disunification: some decidable cases
• Matching Modulo Superdevelopments Application to Second-Order Matching
• Computer Science Logic

Describes a project that uses

Uses Software

• Automath

This page was built for publication: Higher-order beta matching with solutions in long beta-eta normal form

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