Proof Transformation by CERES

DOI10.1007/11812289_8zbMath1125.03012OpenAlexW1544876072MaRDI QIDQ5756761

Alexander Leitsch, Stefan Hetzl, Clemens Richter, Matthias Baaz, 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)

Related Items (8)

Unnamed Item ⋮ Extraction of expansion trees ⋮ CERES: An analysis of Fürstenberg's proof of the infinity of primes ⋮ System Description: The Proof Transformation System CERES ⋮ Extension without cut ⋮ A Clausal Approach to Proof Analysis in Second-Order Logic ⋮ Describing proofs by short tautologies ⋮ Herbrand Sequent Extraction

Uses Software

• CERES

This page was built for publication: Proof Transformation by CERES