System Description: The Proof Transformation System CERES
From MaRDI portal
Publication:5747781
DOI10.1007/978-3-642-14203-1_36zbMath1291.68338MaRDI QIDQ5747781
Alexander Leitsch, Daniel Weller, Bruno Woltzenlogel Paleo, Tomer Libal, Tsvetan Dunchev
Publication date: 14 September 2010
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-14203-1_36
03F05: Cut-elimination and normal-form theorems
Uses Software
Cites Work
- CERES: An analysis of Fürstenberg's proof of the infinity of primes
- Towards a clausal analysis of cut-elimination
- A Clausal Approach to Proof Analysis in Second-Order Logic
- Herbrand Sequent Extraction
- Resolution in type theory
- Logic for Programming, Artificial Intelligence, and Reasoning
- Proof Transformation by CERES
- Cut-elimination and redundancy-elimination by resolution