Representing unification in a logical framework

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

Jason John Brown, Lincoln Wallen

Publication date: 21 June 2024

Mathematics Subject Classification ID

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

Cites Work

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

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

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