RISC-Linz RISC-Linz Research Institute for Symbolic Computation  
about
|
people
|
publications
|
research
|
education
|
industry
|
conferences
|
media
|
projects
internal
  
search:
  
  • @inproceedings{RISC5472,
    author = {David M. Cerna and Michael Lettmann},
    title = {{Towards a Clausal Analysis of Proof Schemata}},
    booktitle = {{SYNASC 2017}},
    language = {english},
    abstract = {Proof schemata are a variant of \LK-proofs able to simulate various induction schemes in first-order logic by adding so called {\em links} to the standard first-order \LK-calculus. Links allow proofs to reference other proofs, and thus give schemata a recursive structure. {\em Gentzen} style cut-elimination methods, which reduce cuts locally, does not work in the presence of links. However, an alternative method, such as cut-elimination by resolution (CERES), which eliminate cuts globally, is able to reduce cuts over the entire recursive structure simultaneously. Unfortunately, analysis of the cut structure of a proof after partial cut-elimination is non-trivial. By extending local methods to proof schemata, we provide such an analysis. },
    series = {IEEE Xplore},
    pages = {--},
    isbn_issn = {KA},
    year = {2017},
    month = {September},
    editor = {KA},
    refereed = {yes},
    length = {8}
    }