Herbrand schemes for cyclic proofs

Abstract Recent work by Afshari et al. introduces 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. The present article generalizes this computational interpretation 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 generalized Herbrand schemes is cyclic proofs, considered here in the context of classical theories of inductively defined predicates. In particular, for cyclic proofs of generalized $\varSigma _{1}$-sequents, Herbrand schemes extract sets of witnessing terms via a simulation of non-wellfounded cut elimination.