A colored version of the λ-calculus

DOI10.1007/3-540-63104-6_30zbMath1430.68412OpenAlexW1554901100MaRDI QIDQ5234713

Michael Kohlhase, Dieter Hutter

Publication date: 1 October 2019

Published in: Automated Deduction—CADE-14 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-63104-6_30

zbMATH Keywords

natural language semanticsproof searchunification problemhead variablesimply-typed lambda calculus with color annotations

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Natural language processing (68T50) Combinatory logic and lambda calculus (03B40) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Productive use of failure in inductive proof

Cites Work

• Unnamed Item
• Unnamed Item
• Rippling: A heuristic for guiding inductive proofs
• Unification under a mixed prefix
• Third order matching is decidable
• Managing structural information by higher-order colored unification
• Productive use of failure in inductive proof