Schemata, Cyclic Proofs and Herbrand Systems
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2606.23040
curl -X POST /api/v1/records/arxiv/2606.23040/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2606.23040/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'