{"id":"arxiv/2606.23040","url":"https://arxiv.org/abs/2606.23040","tags":["cs.LO","math.LO"],"score":0,"title":"Schemata, Cyclic Proofs and Herbrand Systems","domain":"cs.LO","source":"arxiv","authors":["Alexander Leitsch","Anela Lolic","Stella Mahler"],"reviews":0,"subject":"cs.LO","summary":"Inductive proofs can be represented by proof schemata, a formalism that represents infinite sequences of proofs by recursive definitions. Since proof schemata avoid the explicit application of induction rules, they admit novel applications, one of which is the realization of Herbrand's theorem in the presence of induction. In this paper, we develop a new type of proof schema based on point transition systems. For skolemized proof schemata without quantified cuts, so-called Herbrand systems, that is, schemata of Herbrand instances of quantified formulas, can be computed. Herbrand systems also…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-06-22","reactions":{}}