A proof description language and its reduction system

DOI10.2977/PRIMS/1195182986MaRDI QIDQ1055769zbMATH OpenOpenAlexFDO

Authors 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

lambda calculusnormalizationnatural 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)

Cites work

• scientific article; zbMATH DE number 3684934 (Why is no real title available?)
• scientific article; zbMATH DE number 3521950 (Why is no real title available?)
• scientific article; zbMATH DE number 3554266 (Why is no real title available?)
• scientific article; zbMATH DE number 3216998 (Why is no real title available?)
• scientific article; zbMATH DE number 3328156 (Why is no real title available?)
• scientific article; zbMATH DE number 3331288 (Why is no real title available?)
• scientific article; zbMATH DE number 3333259 (Why is no real title available?)
• scientific article; zbMATH DE number 3353249 (Why is no real title available?)
• scientific article; zbMATH DE number 3358455 (Why is no real title available?)
• Minimal and Optimal Computations of Recursive Programs
• On the interpretation of intuitionistic number theory
• Prolegomena to a theory of mechanized formal reasoning
• Recursive Functions and Intuitionistic Number Theory
• The lambda calculus, its syntax and semantics
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES

Cited in

(2)

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

Describes a project that uses

Uses Software

• Automath

This page was built for publication: A proof description language and its reduction system

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1055769)