Mehrsortige logische Systeme mit unendlich langen Formeln I.
Mehrsortige logische Systeme mit unendlich langen Formeln II.
Natural deduction and coherence for non-symmetric linearly distributive categories.
Natural deduction and sequent typed lambda calculus.
Normal Form Theorem for Systems of Sequents
Normalisation of the theory of Cartesian closed categories and conservativity of extensions of
Normalisation of the Theory T of Cartesian Closed Categories and Conservativity of Extensions T[x] of T
Using an inductive definition of normal terms of the theory of Cartesian Closed Categories with a given graph of distinguished morphisms, we give a reduction free proof of the decidability of this theory. This inductive definition enables us to show via functional completeness that extensions of such a theory by new constants (“indeterminates”) are conservative.
Normalization as a consequence of cut elimination
On cut elimination in the presence of peirce rule.
On normalization of proofs in set theory [Book]
On sequent calculi for intuitionistic propositional logic
The well-known Dyckoff's 1992 calculus/procedure for intuitionistic propositional logic is considered and analyzed. It is shown that the calculus is Kripke complete and the procedure in fact works in polynomial space. Then a multi-conclusion intuitionistic calculus is introduced, obtained by adding one new rule to known calculi. A simple proof of Kripke completeness and polynomial-space decidability of this calculus is given. An upper bound on the depth of a Kripke counter-model is obtained.
On two Classical Results in the First Order Logic
Proof theory for full intuitionistic linear logic, bilinear logic, and MIX categories.
Stable surjection logic
Strong functors and interleaving fixpoints in game semantics
We describe a sequent calculus μLJ with primitives for inductive and coinductive datatypes and equip it with reduction rules allowing a sound translation of Gödel’s system T. We introduce the notion of a μ-closed category, relying on a uniform interpretation of open μLJ formulas as strong functors. We show that any μ-closed category is a sound model for μLJ. We then turn to the construction of a concrete μ-closed category based on Hyland-Ong game semantics. The model relies on three main ingredients:...
Strong normalization of barrecursive terms without using infinite terms.
Strong normalization proofs for cut elimination in Gentzen's sequent calculi
We define an equivalent variant of the Gentzen sequent calculus . In weakenings or contractions can be performed in parallel. This modification allows us to interpret a symmetrical system of mix elimination rules by a finite rewriting system; the termination of this rewriting system can be machine checked. We give also a self-contained strong normalization proof by structural induction. We give another strong normalization proof by a strictly monotone subrecursive interpretation; this interpretation...
Theorem Provers for Substructural Logics
Верхние оценки удлинения выводов при устранении сечений
Гейтинговское исчисление предикатов с эпсилон-символом