Researcher in proof theory, logic and complexity
We prove a general form of ‘free-cut elimination’ for first-order theories in linear logic, yielding normal forms of proofs where cuts are anchored to nonlogical steps. To demonstrate the usefulness of this result, we consider a version of arithmetic in linear logic, based on a previous axiomatisation by Bellantoni and Hofmann. We prove a witnessing …
We present deductive systems for various modal logics that can be obtained from the constructive variant of the normal modal logic CK by adding combinations of the axioms d, t, b, 4, and 5. This includes the constructive variants of the standard modal logics K4, S4, and S5. We use for our presentation the formalism …
We show that an adaptation of Peano’s axioms for second-order arithmetic to the language of MSO completely axiomatizes the theory over infinite trees. This continues a line of work begun by Büchi and Siefkes with axiomatizations of MSO over various classes of linear orders. Our proof formalizes, in the axiomatic theory, a translation of MSO …
We consider deep inference proof formalisms, which are flexible enough to embed many widely used proof systems, and construe compression mechanisms `cut’ and `dag’ in a way that is independent of any particular proof system, but in a way that nonetheless has the same effect from the point of view of proof complexity. The main …