17 citations · 18 across the 3 of their papers we have counts for
3 papers
math.LO2025
Unravelling Cyclic First-Order Arithmetic
Graham E. Leigh, Dominik Wehr
Cyclic proof systems for Heyting and Peano arithmetic eschew induction axioms by accepting proofs which are finite graphs rather than trees. Proving that such a cyclic proof system…
math.LO2023★ 1 cited
From GTC to Reset: Generating Reset Proof Systems from Cyclic Proof Systems
Graham E. Leigh, Dominik Wehr
We consider cyclic proof systems in which derivations are graphs rather than trees. Such systems typically come with a condition that isolates which derivations are admitted as 'pr…
cs.LO2020★ 17 cited
Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory (Extended Version)
Yannick Forster, Dominik Kirst, Dominik Wehr
We study various formulations of the completeness of first-order logic phrased in constructive type theory and mechanised in the Coq proof assistant. Specifically, we examine the c…