Herbrand Schemes for Cyclic Proofs
Bahareh Afshari, Sebastian Enqvist, Graham E. Leigh

Abstract:
Recent work by Afshari et al. introduce a notion of Herbrand schemes for first-order logic by associating a higher-order recursion scheme to a sequent calculus proof. Calculating the language of associated Herbrand schemes directly yields Herbrand disjunctions. As such, these schemes can be seen as programs extracted from proofs. In this article, this computational interpretation is explored further by removing the restriction of acyclicity from Herbrand schemes which amounts to admitting recursively defined programs. It is shown that the notion of proof corresponding to these generalised Herbrand schemes is cyclic proofs, considered here in the context of classical theories of inductively defined predicates. In particular, for proofs with end sequents of a form generalising the notion of Σ1-sequents in the first-order setting, Herbrand schemes extract Herbrand expansions from cyclic proofs via a simulation of non-wellfounded cut elimination.