A note on negative tagging for least fixed-point formulae
A Note on Negative Tagging for Least Fixed-Point Formulae
Proof systems with sequents of the form U ⊢ Φ for proving validity of a propositional modal μ-calculus formula Φ over a set U of states in a given model usually handle fixed-point formulae through unfolding, thus allowing such formulae to reappear in a proof. Tagging is a technique originated by Winskel for annotating fixed-point formulae with information about the proof states at which these are unfolded. This information is used later in the proof to avoid unnecessary unfolding, without...
A Proof Procedure for the First Order Logic
Coherence of Proof-net Categories
Entropic Hopf algebras and models of non-commutative logic.
Esquisses et types
Finite sum-product logic.
Functions provably total in
König's Lemma, the ...-rule and primitive recursive arithmetic.
Maximum Cuts in Extended Natural Deduction
Natural deduction and coherence for non-symmetric linearly distributive categories.
Normalization as a consequence of cut elimination
On a unification problem related to Kreisel's conjecture
On global induction mechanisms in a -calculus with explicit approximations
We investigate a Gentzen-style proof system for the first-order -calculus based on cyclic proofs, produced by unfolding fixed point formulas and detecting repeated proof goals. Our system uses explicit ordinal variables and approximations to support a simple semantic induction discharge condition which ensures the well-foundedness of inductive reasoning. As the main result of this paper we propose a new syntactic discharge condition based on traces and establish its equivalence with the semantic...
On global induction mechanisms in a μ-calculus with explicit approximations
We investigate a Gentzen-style proof system for the first-order μ-calculus based on cyclic proofs, produced by unfolding fixed point formulas and detecting repeated proof goals. Our system uses explicit ordinal variables and approximations to support a simple semantic induction discharge condition which ensures the well-foundedness of inductive reasoning. As the main result of this paper we propose a new syntactic discharge condition based on traces and establish its equivalence with the semantic...
On two Classical Results in the First Order Logic
Proof theory for full intuitionistic linear logic, bilinear logic, and MIX categories.
Speed-up for propositional Frege systems via generalizations of proofs
Společný spůsob dokazování různých pouček a vzorců. [I.]
Společný spůsob dokazování různých pouček a vzorců. [II.]