scientific article; zbMATH DE number 1497485
From MaRDI portal
Publication:4499084
apartnesscategorical logicclassical logiccoherence theoremcombinatory logicconnections with computer sciencecut eliminationE-logicfirst-order arithmeticformulas-as-types relationGentzen type systemHilbert-style systeminterpolationintuitionistic logicKleene-style sequent calculuslinear logiclogic programmingminimal logicmodal logicmulti-succedent intuitionistic sequent calculusnatural deduction systemproof theoryresolutionsecond-order Heyting arithmeticsequent calculusstrong normalizationtype theory
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) Combinatory logic and lambda calculus (03B40) Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Proof theory in general (including proof-theoretic semantics) (03F03) Cut-elimination and normal-form theorems (03F05) First-order arithmetic and fragments (03F30) Second- and higher-order arithmetic and fragments (03F35) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Categorical logic, topoi (03G30) Logic programming (68N17)
Recommendations
Cited in
(only showing first 100 items - show all)- Proof theory for admissible rules
- Glivenko theorems revisited
- Let Us investigate! Dynamic conjecture-making as the formal logic of abduction
- Contraction, infinitary quantifiers, and omega paradoxes
- Prehistoric graph in modal derivations and self-referentiality
- 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
- Eliminating disjunctions by disjunction elimination
- A semantic framework for proof evidence
- Proof theory for functional modal logic
- Anything goes
- Goal-oriented proof-search in natural deduction for intuitionistic propositional logic
- Elementary arithmetic
- Multicomponent proof-theoretic method for proving interpolation properties
- Intrinsic reasoning about functional programs. II: Unipolar induction and primitive-recursion
- A spatial logic for concurrency. II
- Glivenko theorems and negative translations in substructural predicate logics
- The power of Belnap: sequent systems for \(SIXTEEN_{3 }\)
- Sequent calculi for intuitionistic Gödel-Löb logic
- Computer says no: verdict explainability for runtime monitors using a local proof system
- Subatomic natural deduction for a naturalistic first-order language with non-primitive identity
- Cut-elimination for weak Grzegorczyk logic Go
- Recapturing dynamic logic of relation changers via bounded morphisms
- Subatomic negation
- What is the meaning of proofs?. A Fregean distinction in proof-theoretic semantics
- 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
- The calculus of natural calculation
- Human-centered automated proof search
- 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
- 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
- Logic and majority voting
- Plotkin's call-by-value \(\lambda\)-calculus as a modal calculus
- 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
- Efficient elimination of Skolem functions in \(\text{LK}^\text{h} \)
- A note on cut-elimination for classical propositional logic
- Uniform Lyndon interpolation for basic non-normal modal logics
- Constructive and mechanised meta-theory of intuitionistic epistemic logic
- Coherence in inquisitive first-order logic
- From truth degree comparison games to sequents-of-relations calculi for Gödel logic
- Essential structure of proofs as a measure of complexity
- Interpolation in extensions of first-order logic
- A type-assignment of linear erasure and duplication
- Herzberger's limit rule with labelled sequent calculus
- Relative full completeness for bicategorical Cartesian closed structure
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Repetition-free and infinitary analytic calculi for first-order rational Pavelka logic
- 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
- A simple logic of functional dependence
- Proof-theoretic semantics and inquisitive logic
- 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
- Noncontractive classical logic
- Absorbing the structural rules in the sequent calculus with additional atomic rules
- Mechanizing focused linear logic in Coq
- Lyndon interpolation theorem of instantial neighborhood logic-constructively via a sequent calculus
- Constructibility of the universal wave function
- Soundness and completeness proofs by coinductive methods
- The Church-Fitch knowability paradox in the light of structural proof theory
- Montague's paradox, informal provability, and explicit modal logic
- \(LE^{t}_{ \to }, LR^{ \circ }_{\widehat{\sim}}, LK\) and cutfree proofs
- Sufficient conditions for cut elimination with complexity analysis
- Making knowledge explicit: how hard it is
- Logic of subtyping
- Computing interpolants in implicational logics
- Incomplete symbols -- definite descriptions revisited
- A simple proof of second-order strong normalization with permutative conversions
- The naturality of natural deduction
- Asymptotic distribution of integers with certain prime factorizations
- On rules
- 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
- Positive logic with adjoint modalities: proof theory, semantics and reasoning about information
- Glivenko sequent classes in the light of structural proof theory
- Imperative LF meta-programming
- 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)
- Sharpened lower bounds for cut elimination
- On the complexity of proof deskolemization
- Tools for the investigation of substructural and paraconsistent logics
- An evaluation-driven decision procedure for G3i
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)
