scientific article; zbMATH DE number 949290

Helmut Schwichtenberg, A. S. Troelstra

Publication date: 25 November 1996

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Modal logic (including the logic of norms) (03B45) 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) Categorical logic, topoi (03G30) Cut-elimination and normal-form theorems (03F05) First-order arithmetic and fragments (03F30) Logic programming (68N17) Second- and higher-order arithmetic and fragments (03F35) Proof theory in general (including proof-theoretic semantics) (03F03) Combinatory logic and lambda calculus (03B40)

Related Items (max. 100)

Sequent Calculus for Intuitionistic Epistemic Logic IEL ⋮ Practical Proof Search for Coq by Type Inhabitation ⋮ CTL Model Checking in Deduction Modulo ⋮ Completeness for a First-Order Abstract Separation Logic ⋮ A NOTE ON THE SEQUENT CALCULI ⋮ Provability multilattice logic ⋮ Rooted hypersequent calculus for modal logic \textsf{S5} ⋮ An ecumenical notion of entailment ⋮ An intuitionistic formula hierarchy based on high‐school identities ⋮ A novel approach to equality ⋮ Complementary proof nets for classical logic ⋮ Cardinality reduction theorem for logics QHC and QH4 ⋮ Linear depth deduction with subformula property for intuitionistic epistemic logic ⋮ The elimination of maximum cuts in linear logic and BCK logic ⋮ Labelled Calculi for Łukasiewicz Logics ⋮ Unnamed Item ⋮ An algebraic glimpse at bunched implications and separation logic ⋮ The Logic of Justification ⋮ Three faces of natural deduction ⋮ COMPLETENESS VIA CORRESPONDENCE FOR EXTENSIONS OF THE LOGIC OF PARADOX ⋮ Kripke semantics for the logic of problems and propositions ⋮ 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 ⋮ CONTRACTION-FREE SEQUENT CALCULI FOR INTUITIONISTIC LOGIC: A CORRECTION ⋮ Unnamed Item ⋮ Comparing Control Constructs by Double-barrelled CPS Transforms ⋮ Towards Hilbert's 24th Problem: Combinatorial Proof Invariants ⋮ SUBFORMULA AND SEPARATION PROPERTIES IN NATURAL DEDUCTION VIA SMALL KRIPKE MODELS ⋮ REPRESENTING CONJUNCTIVE DEDUCTIONS BY DISJUNCTIVE DEDUCTIONS ⋮ THE LOGIC OF JUSTIFICATION ⋮ Interactive Realizability for second-order Heyting arithmetic with EM1 and SK1 ⋮ A natural deduction system for first degree entailment ⋮ Specifying Proof Systems in Linear Logic with Subexponentials ⋮ Dynamical method in algebra: Effective Nullstellensätze ⋮ Unnamed Item ⋮ Intuitionistic logic freed of all metarules ⋮ Proof theory in the abstract ⋮ Completeness of intersection and union type assignment systems for call-by-value \(\lambda\)-models ⋮ On Skolemization in constructive theories ⋮ Coalgebraic Hybrid Logic ⋮ Stoic Sequent Logic and Proof Theory ⋮ MODAL LOGIC WITHOUT CONTRACTION IN A METATHEORY WITHOUT CONTRACTION ⋮ Unnamed Item ⋮ Bounded Linear Logic, Revisited ⋮ Classical mathematics for a constructive world ⋮ INDIRECT PROOF AND INVERSIONS OF SYLLOGISMS ⋮ A Linear-Logical Reconstruction of Intuitionistic Modal Logic S4 ⋮ The normalization theorem for extended natural deduction ⋮ Toward a generalization of the logic of grounding ⋮ Assertions, Hypotheses, Conjectures, Expectations: Rough-Sets Semantics and Proof Theory ⋮ Emptiness and Discharge in Sequent Calculus and Natural Deduction ⋮ Formal explanations as logical derivations ⋮ A Formalisation of Weak Normalisation (with Respect to Permutations) of Sequent Calculus Proofs ⋮ Neo-Logicism and Its Logic ⋮ THE ELIMINATION OF ATOMIC CUTS AND THE SEMISHORTENING PROPERTY FOR GENTZEN’S SEQUENT CALCULUS WITH EQUALITY ⋮ A stone-type duality theorem for separation logic via its underlying bunched logics ⋮ Propositional union closed team logics ⋮ Deep sequent systems for modal logic ⋮ Consequence relations and admissible rules ⋮ Label-free natural deduction systems for intuitionistic and classical modal logics ⋮ Gentzen's consistency proof without heightlines ⋮ A formally verified cut-elimination procedure for linear nested sequents for tense logic ⋮ Algebraic proofs of cut elimination ⋮ Conservativeness and Eliminability for Anti-Realistic Definitions ⋮ A pure view of ecumenical modalities ⋮ Simplifying proofs in Fitch-style natural deduction systems ⋮ Labeled sequent calculus for justification logics ⋮ A generalization of the Lin-Zhao theorem ⋮ Natural deduction calculi and sequent calculi for counterfactual logics ⋮ Variable declarations in natural deduction ⋮ Derivability in certain subsystems of the logic of proofs is \(\Pi_2^p\)-complete ⋮ A herbrandized functional interpretation of classical first-order logic ⋮ A short proof of Glivenko theorems for intermediate predicate logics ⋮ On unification and admissible rules in Gabbay-de Jongh logics ⋮ The problem of \(\Pi_{2}\)-cut-introduction ⋮ Loop-free calculus for modal logic S4. I ⋮ Cut elimination in coalgebraic logics ⋮ Higher-level inferences in the strong-Kleene setting: a proof-theoretic approach ⋮ Conservativity for logics of justified belief: two approaches ⋮ Elementary Proof of Strong Normalization for Atomic F ⋮ Natural deduction for bi-intuitionistic logic ⋮ Proof theory and mathematical meaning of paraconsistent C-systems ⋮ Hybrid logic with the difference modality for generalisations of graphs ⋮ Replacement in logic ⋮ A minimal classical sequent calculus free of structural rules ⋮ The intensional side of algebraic-topological representation theorems ⋮ Proof-theoretic harmony: towards an intensional account ⋮ Grounding principles for (relevant) implication ⋮ Coalgebraic semantics of modal logics: an overview ⋮ Two-sided sequent calculi for \textit{FDE}-like four-valued logics ⋮ On constructing a logic for the notion of complete and immediate formal grounding ⋮ From QBFs to \textsf{MALL} and back via focussing ⋮ Uniform interpolation and sequent calculi in modal logic ⋮ Reasoning processes in propositional logic ⋮ Intuitionistic fixed point logic ⋮ A framework for linear authorization logics ⋮ Interacting explicit evidence systems ⋮ The Skolemization of prenex formulas in intermediate logics ⋮ Herbrand's theorem as higher order recursion

This page was built for publication: