Proof Transformation by CERES

DOI10.1007/11812289_8MaRDI QIDQ5756761zbMATH OpenOpenAlexFDO

Authors Matthias Baaz, Stefan Hetzl, Alexander Leitsch, Clemens Richter, Hendrik Spohr

Publication date 5 September 2007

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

Full work available at URL https://doi.org/10.1007/11812289_8

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05)

Recommendations

• Logic for Programming, Artificial Intelligence, and Reasoning
• System Description: The Proof Transformation System CERES
• CERES in higher-order logic
• Methods of cut-elimination
• scientific article; zbMATH DE number 7178366

Cited in

(15)

• Describing proofs by short tautologies
• Cut-elimination: syntax and semantics
• Fast cut-elimination by CERES
• scientific article; zbMATH DE number 7447752 (Why is no real title available?)
• Cut-elimination and proof schemata
• A Clausal Approach to Proof Analysis in Second-Order Logic
• Proof Transformations and Structural Invariance
• Herbrand Sequent Extraction
• Logic for Programming, Artificial Intelligence, and Reasoning
• Logic for Programming, Artificial Intelligence, and Reasoning
• System Description: The Proof Transformation System CERES
• Extraction of expansion trees
• Extension without cut
• CERES in higher-order logic
• CERES: An analysis of Fürstenberg's proof of the infinity of primes

Describes a project that uses

Uses Software

• CERES

This page was built for publication: Proof Transformation by CERES

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