Proof Transformations and Structural Invariance

DOI10.1007/978-3-540-75939-3_13MaRDI QIDQ5426006zbMATH OpenOpenAlexFDO

Authors Stefan Hetzl, Alexander Leitsch

Publication date 15 November 2007

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-75939-3_13

zbMATH Keywords

profilecut eliminationproof netnegation normal formcharacteristic clause setinvariance under rule permutations

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07)

Recommendations

• Proof Transformation by CERES
• Canonical proof nets for classical logic
• Permutability of proofs in intuitionistic sequent calculi
• Herbrand-confluence
• Identity of Proofs Based on Normalization and Generality

Cites work

• scientific article; zbMATH DE number 3074068 (Why is no real title available?)
• A new deconstructive logic: linear logic
• Computational isomorphisms in classical logic
• Cut normal forms and proof complexity
• Cut-elimination and redundancy-elimination by resolution
• Normal form transformations
• Proof Nets for Classical Logic
• Towards a clausal analysis of cut-elimination

Cited in

(5)

• Describing proofs by short tautologies
• scientific article; zbMATH DE number 67458 (Why is no real title available?)
• Classical proof forestry
• Translating between implicit and explicit versions of proof
• Herbrand Sequent Extraction

This page was built for publication: Proof Transformations and Structural Invariance

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