scientific article; zbMATH DE number 1497485
From MaRDI portal
Publication:4499084
zbMath0957.03053MaRDI QIDQ4499084
Helmut Schwichtenberg, A. S. Troelstra
Publication date: 28 August 2000
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
interpolationmodal logiccut eliminationsequent calculuslinear logicproof theoryresolutionintuitionistic logicnatural deduction systemlogic programmingtype theoryfirst-order arithmeticcategorical logicstrong normalizationclassical logiccombinatory logicminimal logicapartnesscoherence theoremHilbert-style systemE-logicconnections with computer scienceformulas-as-types relationGentzen type systemKleene-style sequent calculusmulti-succedent intuitionistic sequent calculussecond-order Heyting arithmetic
Modal logic (including the logic of norms) (03B45) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Logic in computer science (03B70) Categorical logic, topoi (03G30) Cut-elimination and normal-form theorems (03F05) First-order arithmetic and fragments (03F30) Logic programming (68N17) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Second- and higher-order arithmetic and fragments (03F35) Proof theory in general (including proof-theoretic semantics) (03F03) Combinatory logic and lambda calculus (03B40)
Related Items
On rules, Logic and majority voting, Glivenko sequent classes in the light of structural proof theory, A spatial logic for concurrency. II, Intuitionistic non-normal modal logics: a general framework, De Finettian logics of indicative conditionals. II: Proof theory and algebraic semantics, A more unified approach to free logics, Subminimal logics in light of Vakarelov's logic, 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), Analytic rules for mereology, Let Us investigate! Dynamic conjecture-making as the formal logic of abduction, Proof complexity and textual cohesion, Plotkin's call-by-value \(\lambda\)-calculus as a modal calculus, Fuzzy constructive logic, From input/output logics to conditional logics via sequents -- with provers, Game semantics for constructive modal logic, Sequent calculi for the propositional logic of HYPE, Combinatory logic with polymorphic types, Ordinal arithmetic: Algorithms and mechanization, The Lambek calculus extended with intuitionistic propositional logic, A decidable theory of type assignment, Contraction, infinitary quantifiers, and omega paradoxes, Resource operators for \(\lambda\)-calculus, 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, Prehistoric graph in modal derivations and self-referentiality, Self-referentiality of Brouwer-Heyting-Kolmogorov semantics, A simple sequent calculus for Angell's logic of analytic containment, Four-valued paradefinite logics, Cut elimination, identity elimination, and interpolation in super-Belnap logics, Algorithmic introduction of quantified cuts, Proof systems for Moss' coalgebraic logic, Eliminating disjunctions by disjunction elimination, The Peirce translation, A sequent calculus for a negative free logic, Algebraic proof theory for substructural logics: cut-elimination and completions, Glivenko theorems and negative translations in substructural predicate logics, Dual erotetic calculi and the minimal \(\mathsf{LFI}\), Quantum-like logics and schizophrenia, A semantic framework for proof evidence, Hypersequent calculi for intuitionistic logic with classical atoms, Inhabitation of polymorphic and existential types, Proof theory for functional modal logic, Anything goes, How to assign ordinal numbers to combinatory terms with polymorphic types, The power of Belnap: sequent systems for \(SIXTEEN_{3 }\), On the elimination of quantifier-free cuts, Reasoning about collectively accepted group beliefs, Goal-oriented proof-search in natural deduction for intuitionistic propositional logic, A new model construction by making a detour via intuitionistic theories. I: Operational set theory without choice is \(\Pi_1\)-equivalent to KP, A curious dialogical logic and its composition problem, Deductive verification of alternating systems, Sequent calculi for intuitionistic Gödel-Löb logic, On non-self-referential fragments of modal logics, Constructive belief reports, Computer says no: verdict explainability for runtime monitors using a local proof system, How to deal with unbelievable assertions, Machine semantics, General-elimination stability, Practical extraction of evidence terms from common-knowledge reasoning, A generalized syllogistic inference system based on inclusion and exclusion relations, Kronecker's density theorem and irrational numbers in constructive reverse mathematics, Subatomic natural deduction for a naturalistic first-order language with non-primitive identity, A simple proof of Parsons' theorem, Elementary arithmetic, Cut-elimination for weak Grzegorczyk logic Go, Syntactic cut-elimination for a fragment of the modal mu-calculus, Extension without cut, Recapturing dynamic logic of relation changers via bounded morphisms, CERES in higher-order logic, Self-referential justifications in epistemic logic, On the expressive power of schemes, Corrected upper bounds for free-cut elimination, Subatomic negation, What is the meaning of proofs?. A Fregean distinction in proof-theoretic semantics, Multicomponent proof-theoretic method for proving interpolation properties, On nonmonotonic consequence relations, The implicit commitment of arithmetical theories and its semantic core, The middle ground-ancestral logic, Efficient SAT-based proof search in intuitionistic propositional logic, A note on the unprovability of consistency in formal theories of truth, Proof theory for admissible rules, The calculus of natural calculation, Human-centered automated proof search, Intrinsic reasoning about functional programs. II: Unipolar induction and primitive-recursion, Glivenko theorems revisited, Induction and Skolemization in saturation theorem proving, A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems, SAT-based proof search in intermediate propositional logics, Natural deduction systems for intuitionistic logic with identity, Incomplete symbols -- definite descriptions revisited, 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, Towards a semantic characterization of cut-elimination, Cut elimination for S4C: A case study, The epsilon calculus and Herbrand complexity, The naturality of natural deduction. II: on atomic polymorphism and generalized propositional connectives, Constructibility of the universal wave function, Soundness and completeness proofs by coinductive methods, Brodskio kodavimo metodas teiginių logikai;Brodsky’s coding method for propositional logic, Sharpened lower bounds for cut elimination, On the complexity of proof deskolemization, A NOTE ON FRAGMENTS OF UNIFORM REFLECTION IN SECOND ORDER ARITHMETIC, The naturality of natural deduction, Positive Formulas in Intuitionistic and Minimal Logic, Linear Nested Sequents, 2-Sequents and Hypersequents, Proof-Search in Natural Deduction Calculus for Classical Propositional Logic, Self-referentiality in the Brouwer–Heyting–Kolmogorov Semantics of Intuitionistic Logic, Efficient elimination of Skolem functions in \(\text{LK}^\text{h} \), A note on cut-elimination for classical propositional logic, Intuitionistic Epistemology and Modal Logics of Verification, Asymptotic distribution of integers with certain prime factorizations, Uniform Lyndon interpolation for basic non-normal modal logics, Constructive and mechanised meta-theory of intuitionistic epistemic logic, Infinite-Valued First-Order Łukasiewicz Logic: Hypersequent Calculi Without Structural Rules and Proof Search for Sentences in the Prenex Form, Coherence in inquisitive first-order logic, HOW A SEMANTICS FOR TONK SHOULD BE, A NOTE ON THE SEQUENT CALCULI, From truth degree comparison games to sequents-of-relations calculi for Gödel logic, THE JACOBSON RADICAL OF A PROPOSITIONAL THEORY, Tools for the Investigation of Substructural and Paraconsistent Logics, AN ANALYSIS OF THE RULES OF GENTZEN’SNJANDLJ, An Evaluation-Driven Decision Procedure for G3i, Essential structure of proofs as a measure of complexity, Judgement aggregation in non-classical logics, Interpolation in extensions of first-order logic, Dependently Sorted Logic, Gentzen's Proof of Normalization for Natural Deduction, A type-assignment of linear erasure and duplication, The small‐is‐very‐small principle, Herzberger's limit rule with labelled sequent calculus, Relative full completeness for bicategorical Cartesian closed structure, On structural contraction and why it fails, The placeholder view of assumptions and the Curry-Howard correspondence (extended abstract), Intuitionistic propositional logic with Galois negations, Notes on models of (partial) Kripke-Feferman truth, Unnamed Item, First-order automated reasoning with theories: when deduction modulo theory meets practice, An Investigation into Intuitionistic Logic with Identity, Repetition-free and infinitary analytic calculi for first-order rational Pavelka logic, The Church-Fitch knowability paradox in the light of structural proof theory, Partial and paraconsistent three-valued logics, Unnamed Item, Montague's paradox, informal provability, and explicit modal logic, The New Normal: We Cannot Eliminate Cuts in Coinductive Calculi, But We Can Explore Them, Non-elementary speed-ups in logic calculi, \(LE^{t}_{ \to }, LR^{ \circ }_{\widehat{\sim}}, LK\) and cutfree proofs, Cathoristic Logic, Sufficient conditions for cut elimination with complexity analysis, Machine-Checked Proof-Theory for Propositional Modal Logics, Intuitionistic Decision Procedures Since Gentzen, Consistency, Completeness, and Classicality, Modal and intuitionistic variants of extended Belnap-Dunn logic with classical negation, Natural deduction bottom up, Proof theory for heterogeneous logic combining formulas and diagrams: proof normalization, Cut Elimination for Shallow Modal Logics, A simple logic of functional dependence, Proof-theoretic semantics and inquisitive logic, Generalisation of proof simulation procedures for Frege systems by M.L. Bonet and S.R. Buss, Labelled sequent calculi for Lewis' non-normal propositional modal logics, Extended fuzzy constructive logic, Proofs and countermodels in non-classical logics, Speech acts, categoricity, and the meanings of logical connectives, Hypersequent and display calculi -- a unified perspective, Making knowledge explicit: how hard it is, Logic of subtyping, Unnamed Item, Computing interpolants in implicational logics, A Labeled Natural Deduction System for a Fragment of CTL *, The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem, Aristotle, Logic, and QUARC, Positive Logic with Adjoint Modalities: Proof Theory, Semantics and Reasoning about Information, Unnamed Item, Satisfaction and Friendliness Relations within Classical Logic: Proof-Theoretic Approach, Noncontractive classical logic, Bi-Classical Connexive Logic and its Modal Extension: Cut-elimination, completeness and duality, PROOF SYSTEMS FOR VARIOUS FDE-BASED MODAL LOGICS, FRACTIONAL SEMANTICS FOR CLASSICAL LOGIC, DE MORGAN INTERPRETATION OF THE LAMBEK–GRISHIN CALCULUS, Lexicographic Path Induction, GAME SEMANTICS AND THE GEOMETRY OF BACKTRACKING: A NEW COMPLEXITY ANALYSIS OF INTERACTION, Absorbing the structural rules in the sequent calculus with additional atomic rules, A simple proof of second-order strong normalization with permutative conversions, NATURAL FORMALIZATION: DERIVING THE CANTOR-BERNSTEIN THEOREM IN ZF, Mechanizing focused linear logic in Coq, Lyndon interpolation theorem of instantial neighborhood logic-constructively via a sequent calculus, Free Definite Description Theory – Sequent Calculi and Cut Elimination, Sequent Calculi and Interpolation for Non-Normal Modal and Deontic Logics, Definite Descriptions in Intuitionist Positive Free Logic, Dialogue Games for Minimal Logic, Normalisation for Some Quite Interesting Many-Valued Logics, From Schütte’s Formal Systems to Modern Automated Deduction, Aspects of Categorical Recursion Theory, Geometric Rules in Infinitary Logic, Imperative LF Meta-Programming, Connecting Sequent Calculi with Lorenzen-Style Dialogue Games, THE ELIMINATION OF ATOMIC CUTS AND THE SEMISHORTENING PROPERTY FOR GENTZEN’S SEQUENT CALCULUS WITH EQUALITY, An Arithmetical Interpretation of Verification and Intuitionistic Knowledge, Control effects as a modality, NONCLASSICAL TRUTH WITH CLASSICAL STRENGTH. A PROOF-THEORETIC ANALYSIS OF COMPOSITIONAL TRUTH OVER HYPE, Negative predication and distinctness, Decidable variables for constructive logics, Mechanising Gödel-Löb provability logic in HOL light, Finitary type theories with and without contexts, The placeholder view of assumptions and the Curry-Howard correspondence, A dialogical route to logical pluralism, Cut‐conditions on sets of multiple‐alternative inferences, Forcing revisited, Glivenko sequent classes and constructive cut elimination in geometric logics, Comparing Calculi for First-Order Infinite-Valued Łukasiewicz Logic and First-Order Rational Pavelka Logic, Semantical analysis of the logic of bunched implications, Cut elimination by unthreading, FRACTIONAL-VALUED MODAL LOGIC, The Gödel-McKinsey-Tarski embedding for infinitary intuitionistic logic and its extensions, Towards an intuitionistic deontic logic tolerating conflicting obligations, Is, ought, and cut, Natural deduction calculi for classical and intuitionistic S5, Normalisation and subformula property for a system of intuitionistic logic with general introduction and elimination rules, Game semantics of Martin-Löf type theory, WHAT IS A RULE OF INFERENCE?, Definite Formulae, Negation-as-Failure, and the Base-Extension Semantics of Intuitionistic Propositional Logic, ELIMINATING DISJUNCTIONS BY DISJUNCTION ELIMINATION, Unnamed Item, AXIOMATIC TRUTH, SYNTAX AND METATHEORETIC REASONING, REALIZABILITY SEMANTICS FOR QUANTIFIED MODAL LOGIC: GENERALIZING FLAGG’S 1985 CONSTRUCTION, Strong Normalisation of Cut-Elimination That Simulates β-Reduction, Prawitz, Proofs, and Meaning, Cut Elimination, Substitution and Normalisation, General-Elimination Harmony and Higher-Level Rules, Constructibility and Geometry, Revising a Labelled Sequent Calculus for Public Announcement Logic, Constructive Embedding from Extensions of Logics of Strict Implication into Modal Logics, The Interpretation Existence Lemma, On the unification of classical, intuitionistic and affine logics, Functional Completeness in CPL via Correspondence Analysis, Full Cut Elimination and Interpolation for Intuitionistic Logic with Existence Predicate, Mechanising a Proof of Craig’s Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle, Revisiting Zucker’s Work on the Correspondence Between Cut-Elimination and Normalisation
