scientific article

zbMath0773.03038MaRDI QIDQ3999386

Grigori Mints

Publication date: 23 January 1993

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

natural deductioncategory theoryreflection principlesintuitionistic arithmetictransfinite inductionprogram verificationclosed categoriesnormalization of proofsmodal propositional logictransfinite derivationsHeyting predicate calculusNovikov's hypothesisE-theoremsapplication to computer scienceGentzen's sequence calculusreduction sequence for arithmetic

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Categorical logic, topoi (03G30) Cut-elimination and normal-form theorems (03F05) First-order arithmetic and fragments (03F30) Collected or selected works; reprintings or translations of classics (01A75) Structure of proofs (03F07) Proof theory in general (including proof-theoretic semantics) (03F03) Complexity of proofs (03F20)

Related Items (17)

1998 European Summer Meeting of the Association for Symbolic Logic ⋮ A deep inference system for the modal logic S5 ⋮ Hypersequent rules with restricted contexts for propositional modal logics ⋮ Indexed systems of sequents and cut-elimination ⋮ Essential structure of proofs as a measure of complexity ⋮ A termination proof for epsilon substitution using partial derivations ⋮ Three faces of natural deduction ⋮ A note on Gentzen's ordinal assignment ⋮ Studying provability in implicational intuitionistic logic ⋮ Cut elimination for a simple formulation of epsilon calculus ⋮ Prawitz, Proofs, and Meaning ⋮ Intuitionistic Existential Instantiation and Epsilon Symbol ⋮ Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search ⋮ The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type ⋮ Reduction of finite and infinite derivations ⋮ Some results on cut-elimination, provable well-orderings, induction and reflection ⋮ Aspects of Categorical Recursion Theory

This page was built for publication: