Mechanical procedure for proof construction via closed terms in typed \(\lambda\) calculus

DOI10.1007/BF00244393zbMath0715.03008OpenAlexW2078790484MaRDI QIDQ751646

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)

Related Items

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