David Cerna, Alexander Leitsch,
"Schematic Cut Elimination and the Ordered Pigeonhole Principle"
, in Nicola Olivetti and Ashish Tiwari: Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings, Serie Lecture Notes in Computer Science (LNCS), Vol. 9706, Springer, Seite(n) 241-256, 6-2016, ISSN: 0302-9743
Original Titel:
Schematic Cut Elimination and the Ordered Pigeonhole Principle
Sprache des Titels:
Englisch
Original Buchtitel:
Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings
Original Kurzfassung:
Schematic cut-elimination is a method of cut-elimination which can handle certain types of inductive proofs. In previous work, an attempt was made to apply the schematic CERES method to a formal proof with an arbitrary number of ?2 cuts (a recursive proof encapsulating the infinitary pigeonhole principle). However the derived schematic refutation for the characteristic clause set of the proof could not be expressed in the schematic resolution calculus developed so far. Without this formalization a Herbrand system cannot be algorithmically extracted. In this work, we provide a restriction of infinitary pigeonhole principle, the ECA-schema (Eventually Constant Assertion), or ordered infinitary pigeonhole principle, whose analysis can be completely carried out in the existing framework of schematic CERES. This is the first time the framework is used for proof analysis. From the refutation of the clause set and a substitution schema we construct a Herbrand system.
Forschungs-