A proof description language and its reduction system
From MaRDI portal
Publication:1055769
DOI10.2977/prims/1195182986zbMath0522.03041OpenAlexW2024841767MaRDI QIDQ1055769
Publication date: 1983
Published in: Publications of the Research Institute for Mathematical Sciences, Kyoto University (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.2977/prims/1195182986
normalizationlambda calculusnatural deduction proofs of closed existential formulaeproof description language
Related Items
Proof normalization with nonstandard objects ⋮ Foundation of logic programming based on inductive definition
Uses Software
Cites Work
- Prolegomena to a theory of mechanized formal reasoning
- The lambda calculus, its syntax and semantics
- ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
- Minimal and Optimal Computations of Recursive Programs
- Recursive Functions and Intuitionistic Number Theory
- On the interpretation of intuitionistic number theory
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: A proof description language and its reduction system