RISC RISC Research Institute for Symbolic Computation  
  • @techreport{RISC5592,
    author = {David M. Cerna and Alexander Leitsch and Anela Lolic },
    title = {{A Resolution Calculus for Recursive Clause Sets [Preprint]}},
    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. We provide an example based on an important theoretical case and a procedure for constructing an inessential cut normal form schema.},
    year = {2018},
    month = {Jan.},
    note = {in reiew},
    length = {28},
    type = {RISC Report Series},
    institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
    address = {Schloss Hagenberg, 4232 Hagenberg, Austria}