RISC JKU
  • @techreport{RISC5720,
    author = {David M. Cerna},
    title = {{An Incompleteness Result for Loop Discovery Based Recursive Provers: [Preprint]}}},
    language = {english},
    abstract = {Loop based tableau and resolution provers for recursively defined formula and clause sets have been thoroughly investigated by Aravantinos \textit{et al.} culminating in their work ``A Resolution Calculus for First-order Schemata''. The goal of these methods is to transform the given formula or clause set into a state which is invariant a shift of the free parameter, i.e. $n$ shifted to $n-1$. By invariant, we mean a shift in the value of the free parameter preserving satisfiability. Recent work by Leitsch \textit{et al.} ``CERES for First-Order Schemata'' used a looping resolution prover to transform recursively defined formal proofs into a normal form accepting ``Herbrand sequent'' extraction. While such looping provers can handle expressive classes of recursively defined formulas we show that a quite simple recursive formula resulting from proof transformation can have invariants which cannot be discovered by the discussed loop discovery method. The issue being that any substitution grounding the invariant set of clauses is itself dependent on the free parameter and needs to be shifted as well. This points to a limitation of such loop discovery methods given that quite weak mathematically relevant statements can easily overpower the mechanism.},
    year = {2018},
    month = {july},
    annote = {in review},
    howpublished = {RISC Report},
    length = {27},
    type = {RISC Report Series},
    institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
    address = {Altenberger Straße 69, 4040 Linz, Austria},
    issn = {2791-4267 (online)}
    }