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

Borkowski-Słupecki devicecomputation of a proof over stream objectsexistential elimination ruleformal proof systemsinfinite numbersinfinitely long listslazy computationnatural deductionproof normalization

Mathematics Subject Classification ID

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

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

• A proof description language and its reduction system
• 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?)
• 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)