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}