scientific article; zbMATH DE number 1497485
From MaRDI portal
Publication:4499084
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)
Recommendations
Cited in
(only showing first 100 items - show all)- Towards an intuitionistic deontic logic tolerating conflicting obligations
- Realizability semantics for quantified modal logic: generalizing Flagg's 1985 construction
- Self-referentiality of Brouwer-Heyting-Kolmogorov semantics
- Revisiting Zucker's work on the correspondence between cut-elimination and normalisation
- Constructive embedding from extensions of logics of strict implication into modal logics
- Sequent Calculi and Interpolation for Non-Normal Modal and Deontic Logics
- Revising a labelled sequent calculus for public announcement logic
- Incomplete symbols -- definite descriptions revisited
- Repetition-free and infinitary analytic calculi for first-order rational Pavelka logic
- Glivenko theorems revisited
- Contraction, infinitary quantifiers, and omega paradoxes
- Algorithmic introduction of quantified cuts
- Proof systems for Moss' coalgebraic logic
- The Peirce translation
- Goal-oriented proof-search in natural deduction for intuitionistic propositional logic
- Noncontractive classical logic
- On rules
- Practical extraction of evidence terms from common-knowledge reasoning
- Uniform Lyndon interpolation for basic non-normal modal logics
- Machine semantics
- A note on cut-elimination for classical propositional logic
- A spatial logic for concurrency. II
- 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
- An evaluation-driven decision procedure for G3i
- Cut elimination by unthreading
- Speech acts, categoricity, and the meanings of logical connectives
- Non-labelled sequent calculi of public announcement expansions of \textbf{K45} and \textbf{S5}
- Relative full completeness for bicategorical Cartesian closed structure
- Kronecker's density theorem and irrational numbers in constructive reverse mathematics
- A generalized syllogistic inference system based on inclusion and exclusion relations
- Another combination of classical and intuitionistic conditionals
- A simple proof of second-order strong normalization with permutative conversions
- Computer says no: verdict explainability for runtime monitors using a local proof system
- Proof theory for functional modal logic
- scientific article; zbMATH DE number 7559284 (Why is no real title available?)
- Self-referential justifications in epistemic logic
- Proof-theoretic semantics and inquisitive logic
- Definite descriptions in intuitionist positive free logic
- Algebraic proof theory for substructural logics: cut-elimination and completions
- Lexicographic Path Induction
- Extension without cut
- Quantum-like logics and schizophrenia
- 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
- Glivenko sequent classes and constructive cut elimination in geometric logics
- Fuzzy constructive logic
- The epsilon calculus and Herbrand complexity
- FRACTIONAL-VALUED MODAL LOGIC
- Glivenko sequent classes in the light of structural proof theory
- Game semantics and the geometry of backtracking: a new complexity analysis of interaction
- From Schütte’s Formal Systems to Modern Automated Deduction
- Positive logic with adjoint modalities: proof theory, semantics and reasoning about information
- How a semantics for tonk should be
- Proof theory for admissible rules
- Sequent calculi for choice logics
- Glivenko theorems and negative translations in substructural predicate logics
- Subatomic natural deduction for a naturalistic first-order language with non-primitive identity
- Natural deduction bottom up
- Prawitz, Proofs, and Meaning
- Cut elimination, identity elimination, and interpolation in super-Belnap logics
- Four-valued paradefinite logics
- General-elimination harmony and higher-level rules
- 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)
- Extended fuzzy constructive logic
- Prehistoric graph in modal derivations and self-referentiality
- Denotational semantics of the simplified lambda-mu calculus and a new deduction system of classical type theory
- Cut-elimination for weak Grzegorczyk logic Go
- Proof theory for heterogeneous logic combining formulas and diagrams: proof normalization
- Labelled sequent calculi for Lewis' non-normal propositional modal logics
- An investigation into intuitionistic logic with identity
- A natural deduction calculus for \textbf{S4.2}
- Geometric Rules in Infinitary Logic
- A note on the unprovability of consistency in formal theories of truth
- NONCLASSICAL TRUTH WITH CLASSICAL STRENGTH. A PROOF-THEORETIC ANALYSIS OF COMPOSITIONAL TRUTH OVER HYPE
- Negative predication and distinctness
- On the expressive power of schemes
- NATURAL FORMALIZATION: DERIVING THE CANTOR-BERNSTEIN THEOREM IN ZF
- Dependently Sorted Logic
- Analytic rules for mereology
- Natural deduction systems for intuitionistic logic with identity
- Is, ought, and cut
- Linear Nested Sequents, 2-Sequents and Hypersequents
- Let Us investigate! Dynamic conjecture-making as the formal logic of abduction
- Full cut elimination and interpolation for intuitionistic logic with existence predicate
- From input/output logics to conditional logics via sequents -- with provers
- Self-referentiality in the Brouwer-Heyting-Kolmogorov semantics of intuitionistic logic
- Decidable variables for constructive logics
- Recapturing dynamic logic of relation changers via bounded morphisms
- Synthesizing nested relational queries from implicit specifications: via model theory and via proof theory
- Logic of subtyping
- Proof systems for various \textsf{FDE}-based modal logics
- Corrected upper bounds for free-cut elimination
- Proof complexity and textual cohesion
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- The Church-Fitch knowability paradox in the light of structural proof theory
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)
