Representing unification in a logical framework

DOI10.1007/3-540-61377-3_34zbMATH Open1540.68261MaRDI QIDQ6560164

Jason John Brown, Lincoln Wallen

Publication date: 21 June 2024

Mathematics Subject Classification ID

Logic in computer science (03B70) Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• A proof theory for general unification
• SETHEO: A high-performance theorem prover
• A unification algorithm for typed \(\bar\lambda\)-calculus
• Mechanizing \(\omega\)-order type theory through unification
• Edinburgh LCF. A mechanized logic of computation
• Higher-order unification revisited: Complete sets of transformations
• An Efficient Unification Algorithm
• A framework for defining logics
• Higher-order unification with dependent function types
• A UNIFICATION ALGORITHM FOR THE λΠ-CALCULUS

This page was built for publication: Representing unification in a logical framework