RISC RISC Research Institute for Symbolic Computation  
  • @techreport{RISC5615,
    author = {David M. Cerna and Alexander Leitsch and Anela Lolic },
    title = {{A Resolution Calculus for Recursive Clause Sets: Extended Version}},
    language = {english},
    abstract = {Proof schemata provide an alternative formalism for proofs containing an inductive argument, which allow an extension of Her- brand’s theorem and thus, the construction of Herbrand sequents and ex- pansion trees. Existing proof transformation methods for proof schemata rely on constructing a recursive resolution refutation, a task which is highly non-trivial. An automated method for constructing such refu- tations exists, but only works for a very weak fragment of arithmetic and is hard to use interactively. In this paper we introduce a simplified schematic resolution calculus, based on definitional clause forms allowing interactive construction of refutations beyond existing automated meth- ods. Furthermore we provide a refutation of a recursive clause set, which cannot be finitely represented in existing formalisms.},
    year = {2018},
    month = {April},
    howpublished = {Technical Report},
    length = {28},
    type = {RISC Report Series},
    institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
    address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
    }