Mechanical procedure for proof construction via closed terms in typed calculus

DOI10.1007/BF00244393zbMATH Open0715.03008OpenAlexW2078790484MaRDI QIDQ751646FDOQ751646

Marek Zaionc

Publication date: 1988

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00244393

Recommendations

• scientific article; zbMATH DE number 1670575
• Theorem proving for untyped constructive \(\lambda\)-calculus: Implementation and application
• A typed \(\lambda\)-calculus for proving-by-example and bottom-up generalization procedure
• A coinductive approach to proof search through typed lambda-calculi
• scientific article; zbMATH DE number 4061194
• Proof systems for retracts in simply typed lambda calculus
• Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi
• A semantic characterization of the well-typed formulae of \(\lambda\)- calculus
• scientific article; zbMATH DE number 1301734

zbMATH Keywords

algorithmnatural deduction proofstyped \(\lambda \) calculus

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)

Cited In (5)

• On the expressive power of schemes
• Title not available (Why is that?)
• Title not available (Why is that?)
• Intuitionistic games: determinacy, completeness, and normalization
• Proof-term synthesis on dependent-type systems via explicit substitutions

This page was built for publication: Mechanical procedure for proof construction via closed terms in typed \(\lambda\) calculus

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