@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)}
}