RISC JKU
  • @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 = {Altenberger Straße 69, 4040 Linz, Austria},
    issn = {2791-4267 (online)}
    }