Mechanical procedure for proof construction via closed terms in typed calculus

DOI10.1007/BF00244393MaRDI QIDQ751646zbMATH OpenOpenAlexFDO

Authors 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

zbMATH Keywords

algorithmnatural deduction proofstyped \(\lambda \) calculus

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1670575
• Theorem proving for untyped constructive \(\lambda\)-calculus: Implementation and application
• A typed -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

Cited in

(5)

• scientific article; zbMATH DE number 1670575 (Why is no real title available?)
• Proof-term synthesis on dependent-type systems via explicit substitutions
• On the expressive power of schemes
• scientific article; zbMATH DE number 1670734 (Why is no real title available?)
• Intuitionistic games: determinacy, completeness, and normalization

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)