scientific article; zbMATH DE number 1497485

zbMATH Open0957.03053MaRDI QIDQ4499084FDOQ4499084

Helmut Schwichtenberg, A. S. Troelstra

Publication date: 28 August 2000

Title of this publication is not available (Why is that?)

zbMATH Keywords

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

Mathematics Subject Classification ID

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)

• Noncontractive classical logic
• Goal-oriented proof-search in natural deduction for intuitionistic propositional logic
• The small‐is‐very‐small principle
• The New Normal: We Cannot Eliminate Cuts in Coinductive Calculi, But We Can Explore Them
• Title not available (Why is that?)
• The Interpretation Existence Lemma
• 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
• Machine-Checked Proof-Theory for Propositional Modal Logics
• 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
• An Evaluation-Driven Decision Procedure for G3i
• 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
• 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
• Subatomic negation
• What is the meaning of proofs?. A Fregean distinction in proof-theoretic semantics
• A simple logic of functional dependence
• Logic and majority voting
• Cut Elimination, Substitution and Normalisation
• On nonmonotonic consequence relations
• Human-centered automated proof search
• Mechanizing focused linear logic in Coq
• THE JACOBSON RADICAL OF A PROPOSITIONAL THEORY
• The implicit commitment of arithmetical theories and its semantic core
• The middle ground-ancestral logic
• Efficient SAT-based proof search in intuitionistic propositional logic
• Multicomponent proof-theoretic method for proving interpolation properties
• SAT-based proof search in intermediate propositional logics
• The calculus of natural calculation
• Free Definite Description Theory – Sequent Calculi and Cut Elimination
• Definite Descriptions in Intuitionist Positive Free Logic
• Essential structure of proofs as a measure of complexity
• A type-assignment of linear erasure and duplication
• Satisfaction and Friendliness Relations within Classical Logic: Proof-Theoretic Approach
• Intrinsic reasoning about functional programs. II: Unipolar induction and primitive-recursion
• An Investigation into Intuitionistic Logic with Identity
• Induction and Skolemization in saturation theorem proving
• Anything goes
• A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems
• Dialogue Games for Minimal Logic
• Sequent Calculi and Interpolation for Non-Normal Modal and Deontic Logics
• 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
• AXIOMATIC TRUTH, SYNTAX AND METATHEORETIC REASONING
• 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
• Glivenko theorems and negative translations in substructural predicate logics
• Proof theory for admissible rules
• Positive Formulas in Intuitionistic and Minimal Logic
• 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
• Analytic rules for mereology
• Control effects as a modality
• Judgement aggregation in non-classical logics
• 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
• Montague's paradox, informal provability, and explicit modal logic
• Making knowledge explicit: how hard it is
• Aspects of Categorical Recursion Theory
• HOW A SEMANTICS FOR TONK SHOULD BE
• A sequent calculus for a negative free logic
• The Lambek calculus extended with intuitionistic propositional logic
• Proofs and countermodels in non-classical logics

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)