Representing unification in a logical framework

DOI10.1007/3-540-61377-3_34MaRDI QIDQ6560164zbMATH OpenFDO

Authors 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

• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 51473 (Why is no real title available?)
• scientific article; zbMATH DE number 65531 (Why is no real title available?)
• scientific article; zbMATH DE number 65536 (Why is no real title available?)
• scientific article; zbMATH DE number 482967 (Why is no real title available?)
• scientific article; zbMATH DE number 3331288 (Why is no real title available?)
• A UNIFICATION ALGORITHM FOR THE λΠ-CALCULUS
• A framework for defining logics
• A proof theory for general unification
• A unification algorithm for typed \(\bar\lambda\)-calculus
• An Efficient Unification Algorithm
• Edinburgh LCF. A mechanized logic of computation
• Higher-order unification revisited: Complete sets of transformations
• Higher-order unification with dependent function types
• Mechanizing \(\omega\)-order type theory through unification
• SETHEO: A high-performance theorem prover
• The lambda calculus. Its syntax and semantics. Rev. ed.

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)