Proof normalization with nonstandard objects

DOI10.1016/0304-3975(91)90186-6MaRDI QIDQ1178706zbMATH OpenOpenAlexFDO

Authors Shigeki Goto

Publication date 26 June 1992

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(91)90186-6

zbMATH Keywords

natural deductionproof normalizationinfinite numbers[https://portal.mardi4nfdi.de/w/index.php?title=+Special%3ASearch&search=Borkowski-S%EF%BF%BD%EF%BF%BDupecki+device&go=Go Borkowski-S��upecki device]computation of a proof over stream objectsexistential elimination ruleformal proof systemsinfinitely long listslazy computation

Mathematics Subject Classification ID

Theory of programming languages (68N15) Cut-elimination and normal-form theorems (03F05) Mechanization of proofs and logical operations (03B35) Second- and higher-order arithmetic and fragments (03F35) Nonstandard models of arithmetic (03H15)

Recommendations

• scientific article; zbMATH DE number 512774
• Program extraction from normalization proofs
• scientific article; zbMATH DE number 48365
• Program extraction from proofs of weak head normalization

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 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3360145 (Why is no real title available?)
• A proof description language and its reduction system
• Model theory.
• Non-standard analysis
• Toward automatic program synthesis

Cited in

(2)

• Proof normalization for resolution and paramodulation
• Infinite objects in type theory

This page was built for publication: Proof normalization with nonstandard objects

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