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

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 (3)

• On the expressive power of schemes
• Intuitionistic games: determinacy, completeness, and normalization
• Proof-term synthesis on dependent-type systems via explicit substitutions

Recommendations

• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• A typed \(\lambda\)-calculus for proving-by-example and bottom-up generalization procedure 👍 👎
• A semantic characterization of the well-typed formulae of \(\lambda\)- calculus 👍 👎
• Theorem proving for untyped constructive \(\lambda\)-calculus: Implementation and application 👍 👎
• Proof Systems for Retracts in Simply Typed Lambda Calculus 👍 👎
• Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi 👍 👎
• A coinductive approach to proof search through typed lambda-calculi 👍 👎

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)