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)
- 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
- 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
- The interpretation existence lemma
- The small-is-very-small principle
- The new normal: we cannot eliminate cuts in coinductive calculi, but we can explore them
- 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
- Essential structure of proofs as a measure of complexity
- Satisfaction and Friendliness Relations within Classical Logic: Proof-Theoretic Approach
- Intrinsic reasoning about functional programs. II: Unipolar induction and primitive-recursion
- Cut elimination, substitution and normalisation
- Induction and Skolemization in saturation theorem proving
- Anything goes
- Machine-checked proof-theory for propositional modal logics
- Proof theory. Sequent calculi and related formalisms
- A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems
- Sequent Calculi and Interpolation for Non-Normal Modal and Deontic Logics
- Uniform Lyndon interpolation for basic non-normal modal logics
- A note on cut-elimination for classical propositional logic
- A spatial logic for concurrency. II
- Machine semantics
- A more unified approach to free logics
- De Finettian logics of indicative conditionals. II: Proof theory and algebraic semantics
- Subminimal logics in light of Vakarelov's logic
- Speech acts, categoricity, and the meanings of logical connectives
- Kronecker's density theorem and irrational numbers in constructive reverse mathematics
- A generalized syllogistic inference system based on inclusion and exclusion relations
- A simple proof of second-order strong normalization with permutative conversions
- Proof theory for functional modal logic
- Game semantics and the geometry of backtracking: a new complexity analysis of interaction
- Fuzzy constructive logic
- Cut elimination, identity elimination, and interpolation in super-Belnap logics
- Four-valued paradefinite logics
- Denotational semantics of the simplified lambda-mu calculus and a new deduction system of classical type theory
- A note on the unprovability of consistency in formal theories of truth
- Full cut elimination and interpolation for intuitionistic logic with existence predicate
- Decidable variables for constructive logics
- On the expressive power of schemes
- From input/output logics to conditional logics via sequents -- with provers
- Let Us investigate! Dynamic conjecture-making as the formal logic of abduction
- Logic of subtyping
- Intuitionistic epistemology and modal logics of verification
- Aristotle, logic, and QUARC
- Consistency, completeness, and classicality
- Constructive and mechanised meta-theory of intuitionistic epistemic logic
- Notes on models of (partial) Kripke-Feferman truth
- Title not available (Why is that?)
- \(LE^{t}_{ \to }, LR^{ \circ }_{\widehat{\sim}}, LK\) and cutfree proofs
- Computing interpolants in implicational logics
- Soundness and completeness proofs by coinductive methods
- Hypersequent and display calculi -- a unified perspective
- Partial and paraconsistent three-valued logics
- Dual erotetic calculi and the minimal \(\mathsf{LFI}\)
- Sequent calculi for intuitionistic Gödel-Löb logic
- Interpolation in extensions of first-order logic
- Title not available (Why is that?)
- Finitary type theories with and without contexts
- Proof-Search in Natural Deduction Calculus for Classical Propositional Logic
- Intuitionistic non-normal modal logics: a general framework
- The Gödel-McKinsey-Tarski embedding for infinitary intuitionistic logic and its extensions
- Cut elimination for shallow modal 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)
