A proof description language and its reduction system

DOI10.2977/prims/1195182986zbMath0522.03041OpenAlexW2024841767MaRDI QIDQ1055769

Masami Hagiya

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

zbMATH Keywords

normalizationlambda calculusnatural deduction proofs of closed existential formulaeproof description language

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Combinatory logic and lambda calculus (03B40)

Related Items

Proof normalization with nonstandard objects ⋮ Foundation of logic programming based on inductive definition

Uses Software

• Automath

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