scientific article; zbMATH DE number 949290
From MaRDI portal
Publication:4716271
interpolationtype theorysecond order Heyting arithmeticproof theorynormalizationnatural deduction systemmultisetsmodal logicminimal logiclogic programminglinear logicintiutionistic logiccategorical logicHilbert style systemGentzen type systemformulas-as-types relationfirst order arithmeticcut eliminationcontextsconnections with computer sciencecombinatory logiccoherence theoremclassical logic
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) 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) Categorical logic, topoi (03G30) Logic programming (68N17)
Recommendations
Cited in
(only showing first 100 items - show all)- Counting proofs in propositional logic
- A solver for QBFs in negation normal form
- The many faces of interpolation
- Normal derivations and sequent derivations
- Focusing and polarization in linear, intuitionistic, and classical logics
- Commuting conversions vs. the standard conversions of the ``good connectives
- Normal functors, power series and -calculus
- On the shape of mathematical arguments
- Handbook of proof theory
- Permutability of proofs in intuitionistic sequent calculi
- Algebraic proofs of cut elimination
- Harmony and autonomy in classical logic
- Correspondences between classical, intuitionistic and uniform provability
- Higher type recursion, ramification and polynomial time
- Doing logic by computer: Interpolation in fragments of intuitionistic propositional logic
- The problem of \(\Pi_{2}\)-cut-introduction
- Natural deduction for bi-intuitionistic logic
- On constructing a logic for the notion of complete and immediate formal grounding
- Uniform interpolation and sequent calculi in modal logic
- The Skolemization of prenex formulas in intermediate logics
- Paraconsistent informational logic
- Natural deduction for first-order hybrid logic
- Perpetuality and uniform normalization in orthogonal rewrite systems
- Conservation and uniform normalization in lambda calculi with erasing reductions
- Church-Rosser property of a simple reduction for full first-order classical natural deduction
- Replacement in logic
- Reasoning processes in propositional logic
- Herbrand's theorem as higher order recursion
- Symmetric bimonoidal intermuting categories and \(\omega\times\omega\) reduced bar constructions
- Proof search and certificates for evidential transactions
- Grounding, quantifiers, and paradoxes
- Cut-free sequent calculus and natural deduction for the tetravalent modal logic
- Cut elimination for systems of transparent truth with restricted initial sequents
- Maximum segments as natural deduction images of some cuts
- Leśniewski's ontology -- proof-theoretic characterization
- The G4i analogue of a G3i sequent calculus
- A stone-type duality theorem for separation logic via its underlying bunched logics
- Propositional union closed team logics
- A formally verified cut-elimination procedure for linear nested sequents for tense logic
- A pure view of ecumenical modalities
- From QBFs to \textsf{MALL} and back via focussing
- Intuitionistic fixed point logic
- Hybrid-logical reasoning in the Smarties and Sally-Anne tasks
- Absorbing the structural rules in the sequent calculus with additional atomic rules
- An analytic calculus for the intuitionistic logic of proofs
- Term-generic logic
- Non-circular proofs and proof realization in modal logic
- Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models
- Why ramify?
- Gentzen's consistency proof without heightlines
- A herbrandized functional interpretation of classical first-order logic
- A framework for linear authorization logics
- Full classical S5 in natural deduction with weak normalization
- On the unity of duality
- Decision methods for linearly ordered Heyting algebras
- Typing in reflective combinatory logic
- Justified common knowledge
- Validity concepts in proof-theoretic semantics
- The Skolemization of existential quantifiers in intuitionistic logic
- Intuitionistic hybrid logic
- Deciding regular grammar logics with converse through first-order logic
- Order-enriched categorical models of the classical sequent calculus
- Higher-level inferences in the strong-Kleene setting: a proof-theoretic approach
- The intensional side of algebraic-topological representation theorems
- Proof-theoretic harmony: towards an intensional account
- Grounding principles for (relevant) implication
- Two-sided sequent calculi for \textit{FDE}-like four-valued logics
- An infinitary system for the least fixed-point logic restricted to finite models
- Admissibility of cut in coalgebraic logics
- Label-free natural deduction systems for intuitionistic and classical modal logics
- Conservativeness and eliminability for anti-realistic definitions. Towards a global view of the meaning of logical constants
- An elementary proof of strong normalization for atomic F
- The Logic of Justification
- Consequence relations and admissible rules
- Kripke Semantics for Basic Sequent Systems
- On the proof complexity of cut-free bounded deep inference
- A Hypersequent System for Gödel-Dummett Logic with Non-constant Domains
- Classical mathematics for a constructive world
- Proofs and computations
- Stone-type dualities for separation logics
- scientific article; zbMATH DE number 432699 (Why is no real title available?)
- The blind spot. Lectures on logic
- Completeness for a first-order abstract separation logic
- Kripke semantics for the logic of problems and propositions
- Labeled sequent calculus for justification logics
- Natural deduction calculi and sequent calculi for counterfactual logics
- CTL model checking in deduction modulo
- Labelled Calculi for Łukasiewicz Logics
- Subformula and separation properties in natural deduction via small Kripke models
- The logic of justification
- On Skolemization in constructive theories
- Coalgebraic Hybrid Logic
- scientific article; zbMATH DE number 4004176 (Why is no real title available?)
- scientific article; zbMATH DE number 4033738 (Why is no real title available?)
- A short proof of Glivenko theorems for intermediate predicate logics
- On unification and admissible rules in Gabbay-de Jongh logics
- Loop-free calculus for modal logic S4. I
- scientific article; zbMATH DE number 42059 (Why is no real title available?)
- scientific article; zbMATH DE number 48365 (Why is no real title available?)
- Conservativity for logics of justified belief: two approaches
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 Q4716271)
