CERES

System description: the proof transformation system CERES. Cut-elimination is the most prominent form of proof transformation in logic. The elimination of cuts in formal proofs corresponds to the removal of intermediate statements (lemmas) in mathematical proofs. The cut-elimination method CERES (cut-elimination by resolution) works by extracting a set of clauses from a proof with cuts. Any resolution refutation of this set then serves as a skeleton of an ACNF, an LK-proof with only atomic cuts. The system CERES, an implementation of the CERES-method has been used successfully in analyzing nontrivial mathematical proofs (see [M. Baaz et al., Theor. Comput. Sci. 403, No. 2–3, 160–175 (2008; Zbl 1181.68264)]). In this paper we describe the main features of the CERES system with special emphasis on the extraction of Herbrand sequents and simplification methods on these sequents. We demonstrate the Herbrand sequent extraction and simplification by a mathematical example.


References in zbMATH (referenced in 16 articles )

Showing results 1 to 16 of 16.
Sorted by year (citations)

  1. Cerna, David; Leitsch, Alexander; Reis, Giselle; Wolfsteiner, Simon: Ceres in intuitionistic logic (2017)
  2. Peltier, N.: A paramodulation-based calculus for refuting schemata of clause sets defined by rewrite rules (2017)
  3. Woltzenlogel Paleo, Bruno: Reducing redundancy in cut-elimination by resolution (2017)
  4. Cerna, David M.; Leitsch, Alexander: Schematic cut elimination and the ordered pigeonhole principle (2016)
  5. Ebner, Gabriel; Hetzl, Stefan; Reis, Giselle; Riener, Martin; Wolfsteiner, Simon; Zivota, Sebastian: System description: GAPT 2.0 (2016)
  6. Cerna, David: A tableaux-based decision procedure for multi-parameter propositional schemata (2014)
  7. Hetzl, Stefan; Straßburger, Lutz: Herbrand-confluence (2013)
  8. Straßburger, Lutz: Extension without cut (2012)
  9. Hetzl, Stefan; Leitsch, Alexander; Weller, Daniel: CERES in higher-order logic (2011)
  10. Dunchev, Tsvetan; Leitsch, Alexander; Libal, Tomer; Weller, Daniel; Woltzenlogel Paleo, Bruno: System description: the proof transformation system CERES (2010)
  11. Hetzl, Stefan: On the form of witness terms (2010)
  12. Hetzl, Stefan: Describing proofs by short tautologies (2009)
  13. Hetzl, Stefan; Leitsch, Alexander; Weller, Daniel; Woltzenlogel Paleo, Bruno: A clausal approach to proof analysis in second-order logic (2009)
  14. Baaz, Matthias; Hetzl, Stefan; Leitsch, Alexander; Richter, Clemens; Spohr, Hendrik: CERES: An analysis of Fürstenberg’s proof of the infinity of primes (2008)
  15. Baaz, Matthias; Hetzl, Stefan; Leitsch, Alexander; Richter, Clemens; Spohr, Hendrik: Proof transformation by CERES (2006)
  16. Baaz, Matthias; Hetzl, Stefan; Leitsch, Alexander; Richter, Clemens; Spohr, Hendrik: Cut-elimination: experiments with CERES (2005)