scientific article; zbMATH DE number 949290
zbMATH Open0868.03024MaRDI QIDQ4716271FDOQ4716271
Authors: A. S. Troelstra, Helmut Schwichtenberg 
Publication date: 25 November 1996
Title of this publication is not available (Why is that?)
Recommendations
interpolationproof theorycategorical logiccombinatory logiclinear logicmodal logictype theorycut eliminationnormalizationclassical logiclogic programmingminimal logicmultisetscontextsfirst order arithmeticcoherence theoremnatural deduction systemconnections with computer scienceformulas-as-types relationGentzen type systemHilbert style systemintiutionistic logicsecond 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) First-order arithmetic and fragments (03F30) 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)
- Loop-free calculus for modal logic S4. I
- Interacting explicit evidence systems
- Symmetric bimonoidal intermuting categories and \(\omega\times\omega\) reduced bar constructions
- CONTRACTION-FREE SEQUENT CALCULI FOR INTUITIONISTIC LOGIC: A CORRECTION
- Title not available (Why is that?)
- Hybrid logic with the difference modality for generalisations of graphs
- On unification and admissible rules in Gabbay-de Jongh logics
- The Skolemization of existential quantifiers in intuitionistic logic
- Derivability in certain subsystems of the logic of proofs is \(\Pi_2^p\)-complete
- Proof theory and mathematical meaning of paraconsistent C-systems
- Labelled Calculi for Łukasiewicz Logics
- Consequence relations and admissible rules
- Church-Rosser property of a simple reduction for full first-order classical natural deduction
- Deciding regular grammar logics with converse through first-order logic
- The Logic of Justification
- An analytic calculus for the intuitionistic logic of proofs
- Simplifying proofs in Fitch-style natural deduction systems
- Coalgebraic Hybrid Logic
- On the shape of mathematical arguments
- Completeness via correspondence for extensions of the logic of paradox
- Non-circular proofs and proof realization in modal logic
- Decision methods for linearly ordered Heyting algebras
- On Skolemization in constructive theories
- Exception tracking in an open world
- Harmony and autonomy in classical logic
- Propositional union closed team logics
- Label-free natural deduction systems for intuitionistic and classical modal logics
- Cut-free sequent calculus and natural deduction for the tetravalent modal logic
- Validity concepts in proof-theoretic semantics
- Proof analysis in modal logic
- Proofs and computations
- Coalgebraic semantics of modal logics: an overview
- Higher type recursion, ramification and polynomial time
- Interactive realizability for second-order Heyting arithmetic with EM1 and SK1
- The many faces of interpolation
- Dynamical method in algebra: Effective Nullstellensätze
- The normalization theorem for extended natural deduction
- Neo-Logicism and Its Logic
- On the proof complexity of cut-free bounded deep inference
- Correspondences between classical, intuitionistic and uniform provability
- Justified common knowledge
- Intuitionistic hybrid logic
- Permutability of proofs in intuitionistic sequent calculi
- The blind spot. Lectures on logic
- Specifying proof systems in linear logic with subexponentials
- Resolution is cut-free
- Labeled sequent calculus for justification logics
- Natural deduction calculi and sequent calculi for counterfactual logics
- The logic of justification
- Conservativity for logics of justified belief: two approaches
- Admissibility of cut in coalgebraic logics
- Title not available (Why is that?)
- Sequent calculi and decidability for intuitionistic hybrid logic
- Towards Hilbert's 24th Problem: Combinatorial Proof Invariants
- A natural deduction system for first degree entailment
- Paraconsistent informational logic
- A minimal classical sequent calculus free of structural rules
- Kripke Semantics for Basic Sequent Systems
- Cut elimination in coalgebraic logics
- Completeness of intersection and union type assignment systems for call-by-value \(\lambda\)-models
- Gentzen calculi for the existence predicate
- Focusing and polarization in linear, intuitionistic, and classical logics
- Intuitionistic logic freed of all metarules
- Deep sequent systems for modal logic
- Full classical S5 in natural deduction with weak normalization
- A solver for QBFs in negation normal form
- Title not available (Why is that?)
- Proof theory of Nelson's paraconsistent logic: a uniform perspective
- Natural deduction for first-order hybrid logic
- Normal functors, power series and \(\lambda\)-calculus
- Algebraic proofs of cut elimination
- Abstract deduction and inferential models for type theory
- On the unity of duality
- A short proof of Glivenko theorems for intermediate predicate logics
- Order-enriched categorical models of the classical sequent calculus
- On defining the notion of complete and immediate formal grounding
- Uniform interpolation and sequent calculi in modal logic
- Proof-theoretic functional completeness for the hybrid logics of everywhere and elsewhere
- Propositional team logics
- Herbrand's theorem as higher order recursion
- Conservation and uniform normalization in lambda calculi with erasing reductions
- Perpetuality and uniform normalization in orthogonal rewrite systems
- The G4i analogue of a G3i sequent calculus
- Provably recursive functions of constructive and relatively constructive theories
- Hybrid-logical reasoning in the Smarties and Sally-Anne tasks
- Cut elimination for systems of transparent truth with restricted initial sequents
- \(\mathcal {BCDL}\): Basic constructive description logic
- A herbrandized functional interpretation of classical first-order logic
- The Skolemization of prenex formulas in intermediate logics
- Stone-type dualities for separation logics
- Common knowledge does not have the Beth property
- Assertions, Hypotheses, Conjectures, Expectations: Rough-Sets Semantics and Proof Theory
- A generalization of the Lin-Zhao theorem
- Proof theory in the abstract
- Variable declarations in natural deduction
- Proof-theoretic harmony: towards an intensional account
- A formally verified cut-elimination procedure for linear nested sequents for tense logic
- A stone-type duality theorem for separation logic via its underlying bunched logics
- Counting proofs in propositional logic
- A pure view of ecumenical modalities
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)
