An Infinitary and a Cyclic Sequent Calculus for Non-Monotone Inductive Definitions
Inductive definitions are an important form of knowledge in mathematics and computer science. Two common techniques to prove theorems about inductive definitions are the principle of mathematical induction and the principle of infinite descent. To formalize these principles, Brotherston and Simpson introduced the sequent calculus proof systems LKID, for mathematical induction, and LKIDω and CLKIDω , for infinite descent. LKIDω is an infinitary system, in which proofs are infinite trees, and CLKIDω a cyclic system, in which proofs are finite graphs. However, these calculi restrict to monotone…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2609.26337
curl -X POST /api/v1/records/arxiv/2609.26337/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2609.26337/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'