scientific article; zbMATH DE number 1497485
zbMATH Open0957.03053MaRDI QIDQ4499084FDOQ4499084
Authors: A. S. Troelstra, Helmut Schwichtenberg 
Publication date: 28 August 2000
Title of this publication is not available (Why is that?)
Recommendations
interpolationproof theoryresolutioncategorical logiccombinatory logicintuitionistic logiclinear logicmodal logictype theorycut eliminationstrong normalizationsequent calculusclassical logiclogic programmingminimal logicapartnessfirst-order arithmeticcoherence theoremHilbert-style systemnatural deduction systemE-logicconnections with computer scienceformulas-as-types relationGentzen type systemKleene-style sequent calculusmulti-succedent intuitionistic sequent calculussecond-order Heyting arithmetic
Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Modal logic (including the logic of norms) (03B45) Proof theory in general (including proof-theoretic semantics) (03F03) Cut-elimination and normal-form theorems (03F05) Logic programming (68N17) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) First-order arithmetic and fragments (03F30) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Categorical logic, topoi (03G30) Second- and higher-order arithmetic and fragments (03F35) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01)
Cited In (only showing first 100 items - show all)
- Self-referentiality of Brouwer-Heyting-Kolmogorov semantics
- Incomplete symbols -- definite descriptions revisited
- Contraction, infinitary quantifiers, and omega paradoxes
- Glivenko theorems revisited
- Algorithmic introduction of quantified cuts
- Proof systems for Moss' coalgebraic logic
- The Peirce translation
- Practical extraction of evidence terms from common-knowledge reasoning
- On rules
- Relative full completeness for bicategorical Cartesian closed structure
- Proof-theoretic semantics and inquisitive logic
- Self-referential justifications in epistemic logic
- Algebraic proof theory for substructural logics: cut-elimination and completions
- Extension without cut
- Quantum-like logics and schizophrenia
- The epsilon calculus and Herbrand complexity
- Positive logic with adjoint modalities: proof theory, semantics and reasoning about information
- Glivenko sequent classes in the light of structural proof theory
- How a semantics for tonk should be
- Glivenko theorems and negative translations in substructural predicate logics
- Proof theory for admissible rules
- General-elimination harmony and higher-level rules
- Extended fuzzy constructive logic
- A simple proof of Parsons' theorem
- Cut elimination for GLS using the terminability of its regress process
- Natural deduction for the Sheffer stroke and Peirce's arrow (and any other truth-functional connective)
- Geometric Rules in Infinitary Logic
- Prehistoric graph in modal derivations and self-referentiality
- Self-referentiality in the Brouwer-Heyting-Kolmogorov semantics of intuitionistic logic
- Analytic rules for mereology
- Proof systems for various \textsf{FDE}-based modal logics
- Control effects as a modality
- Judgement aggregation in non-classical logics
- Formalized proof systems for propositional logic
- The Church-Fitch knowability paradox in the light of structural proof theory
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Corrected upper bounds for free-cut elimination
- Proof complexity and textual cohesion
- The power of Belnap: sequent systems for \(SIXTEEN_{3 }\)
- Non-elementary speed-ups in logic calculi
- Axiomatic truth, syntax and metatheoretic reasoning
- Montague's paradox, informal provability, and explicit modal logic
- Making knowledge explicit: how hard it is
- A sequent calculus for a negative free logic
- The Lambek calculus extended with intuitionistic propositional logic
- Proofs and countermodels in non-classical logics
- On the complexity of proof deskolemization
- A new model construction by making a detour via intuitionistic theories. I: Operational set theory without choice is \(\Pi_1\)-equivalent to KP
- Reasoning about collectively accepted group beliefs
- Syntactic cut-elimination for a fragment of the modal mu-calculus
- A curious dialogical logic and its composition problem
- Constructibility and Geometry
- Ordinal arithmetic: Algorithms and mechanization
- Towards a semantic characterization of cut-elimination
- Gentzen's Proof of Normalization for Natural Deduction
- Sufficient conditions for cut elimination with complexity analysis
- Sharpened lower bounds for cut elimination
- A decidable theory of type assignment
- How to assign ordinal numbers to combinatory terms with polymorphic types
- On non-self-referential fragments of modal logics
- A proof-search procedure for intuitionistic propositional logic
- Does the deduction theorem fail for modal logic?
- Analytic calculi for circular concepts by finite revision
- Socratic trees
- Positive formulas in intuitionistic and minimal logic
- Constructive belief reports
- Aspects of categorical recursion theory
- On the unification of classical, intuitionistic and affine logics
- General-elimination stability
- Towards an intuitionistic deontic logic tolerating conflicting obligations
- Revising a labelled sequent calculus for public announcement logic
- How to deal with unbelievable assertions
- Noncontractive classical logic
- Goal-oriented proof-search in natural deduction for intuitionistic propositional logic
- An evaluation-driven decision procedure for G3i
- Title not available (Why is that?)
- Definite descriptions in intuitionist positive free logic
- Computer says no: verdict explainability for runtime monitors using a local proof system
- A binary quantifier for definite descriptions for cut free free logics
- Normalisation and subformula property for a system of classical logic with Tarski's rule
- The naturality of natural deduction. II: on atomic polymorphism and generalized propositional connectives
- From Schütte’s Formal Systems to Modern Automated Deduction
- Subatomic natural deduction for a naturalistic first-order language with non-primitive identity
- An investigation into intuitionistic logic with identity
- Cut-elimination for weak Grzegorczyk logic Go
- NATURAL FORMALIZATION: DERIVING THE CANTOR-BERNSTEIN THEOREM IN ZF
- Linear Nested Sequents, 2-Sequents and Hypersequents
- Natural deduction systems for intuitionistic logic with identity
- Recapturing dynamic logic of relation changers via bounded morphisms
- AN ANALYSIS OF THE RULES OF GENTZEN’SNJANDLJ
- Semantical analysis of the logic of bunched implications
- Plotkin's call-by-value \(\lambda\)-calculus as a modal calculus
- Combinatory logic with polymorphic types
- Efficient elimination of Skolem functions in \(\text{LK}^\text{h} \)
- Sequent calculi for the propositional logic of HYPE
- Dialogue games for minimal logic
- From truth degree comparison games to sequents-of-relations calculi for Gödel logic
- Lyndon interpolation theorem of instantial neighborhood logic-constructively via a sequent calculus
- Intuitionistic Decision Procedures Since Gentzen
- Elementary arithmetic
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4499084)
