scientific article

Publication date: 18 September 2001

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

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Structure of proofs (03F07)

Related Items

Dialogues and Proofs; Yankov’s Contribution to Proof Theory ⋮ A Cut-Free Labelled Sequent Calculus for Dynamic Epistemic Logic ⋮ A dual-context sequent calculus for the constructive modal logic S4 ⋮ Equality and Apartness in Bi-intuitinistic Logic ⋮ The Rule of Existential Generalisation and Explicit Substitution ⋮ The Jacobson radical for an inconsistency predicate ⋮ A NOTE ON THE SEQUENT CALCULI ⋮ THE JACOBSON RADICAL OF A PROPOSITIONAL THEORY ⋮ LINEAR TIME IN HYPERSEQUENT FRAMEWORK ⋮ Provability multilattice logic ⋮ NONCLASSICAL TRUTH WITH CLASSICAL STRENGTH. A PROOF-THEORETIC ANALYSIS OF COMPOSITIONAL TRUTH OVER HYPE ⋮ ABSTRACT FORMS OF QUANTIFICATION IN THE QUANTIFIED ARGUMENT CALCULUS ⋮ RUSSELLIAN DEFINITE DESCRIPTION THEORY—A PROOF THEORETIC APPROACH ⋮ Mechanising Gödel-Löb provability logic in HOL light ⋮ SUBATOMIC INFERENCES: AN INFERENTIALIST SEMANTICS FOR ATOMICS, PREDICATES, AND NAMES ⋮ A Survey of the Proof-Theoretic Foundations of Logic Programming ⋮ The placeholder view of assumptions and the Curry-Howard correspondence ⋮ An ecumenical notion of entailment ⋮ Proof-theoretic pluralism ⋮ A first-order expansion of Artemov and Protopopescu's intuitionistic epistemic logic ⋮ Wansing's bi-intuitionistic logic: semantics, extension and unilateralisation ⋮ Paraconsistent logic and query answering in inconsistent databases ⋮ A note on decidability of variables in intuitionistic propositional logic ⋮ An infinity of intuitionistic connexive logics ⋮ A novel approach to equality ⋮ Bisequent calculus for four-valued quasi-relevant logics: cut elimination and interpolation ⋮ Non-transitive correspondence analysis ⋮ The elimination of maximum cuts in linear logic and BCK logic ⋮ Is, ought, and cut ⋮ Normalisation and subformula property for a system of intuitionistic logic with general introduction and elimination rules ⋮ Core Type Theory ⋮ On Synonymy in Proof-Theoretic Semantics: The Case of \(\mathtt{2Int}\) ⋮ An Investigation into Intuitionistic Logic with Identity ⋮ Proof Terms for Generalized Natural Deduction ⋮ Book review of: J. von Plato, Elements of logical reasoning ⋮ From mathematical axioms to mathematical rules of proof: recent developments in proof analysis ⋮ Stoic Sequent Logic and Proof Theory ⋮ A new connective in natural deduction, and its application to quantum computing ⋮ Prawitz, Proofs, and Meaning ⋮ Cut Elimination, Substitution and Normalisation ⋮ Inversion Principles and Introduction Rules ⋮ Meaning in Use ⋮ General-Elimination Harmony and Higher-Level Rules ⋮ Constructibility and Geometry ⋮ Revising a Labelled Sequent Calculus for Public Announcement Logic ⋮ Constructive Embedding from Extensions of Logics of Strict Implication into Modal Logics ⋮ Fregean Description Theory in Proof-Theoretical Setting ⋮ PROOF-THEORETIC ANALYSIS OF THE QUANTIFIED ARGUMENT CALCULUS ⋮ Deriving Natural Deduction Rules from Truth Tables ⋮ Axiomatic and dual systems for constructive necessity, a formally verified equivalence ⋮ The normalization theorem for extended natural deduction ⋮ Functional Completeness in CPL via Correspondence Analysis ⋮ Full Cut Elimination and Interpolation for Intuitionistic Logic with Existence Predicate ⋮ Structural proof theory for first-order weak Kleene logics ⋮ Generalized Elimination Inferences, Higher-Level Rules, and the Implications-as-Rules Interpretation of the Sequent Calculus ⋮ Revisiting Zucker’s Work on the Correspondence Between Cut-Elimination and Normalisation ⋮ Free Definite Description Theory – Sequent Calculi and Cut Elimination ⋮ Sequent Calculi and Interpolation for Non-Normal Modal and Deontic Logics ⋮ Logical Nihilism and the Logic of ‘prem’ ⋮ Geometric Rules in Infinitary Logic ⋮ CUT ELIMINATION AND NORMALIZATION FOR GENERALIZED SINGLE AND MULTI-CONCLUSION SEQUENT AND NATURAL DEDUCTION CALCULI ⋮ THE ELIMINATION OF ATOMIC CUTS AND THE SEMISHORTENING PROPERTY FOR GENTZEN’S SEQUENT CALCULUS WITH EQUALITY ⋮ CALCULIZING CLASSICAL INFERENTIAL EROTETIC LOGIC ⋮ Sequent Calculus for Euler Diagrams ⋮ Logic and majority voting ⋮ Socratic proofs ⋮ Proof analysis of Peirce's alpha system of graphs ⋮ Correspondence analysis for some fragments of classical propositional logic ⋮ Glivenko sequent classes in the light of structural proof theory ⋮ A more unified approach to free logics ⋮ On all strong Kleene generalizations of classical logic ⋮ A proof theoretic view of spatial and temporal dependencies in biochemical systems ⋮ Analytic rules for mereology ⋮ Logicality, double-line rules, and modalities ⋮ Sequent calculi for the propositional logic of HYPE ⋮ Introspection, Normality and Agglomeration ⋮ CONDITIONAL BELIEFS: FROM NEIGHBOURHOOD SEMANTICS TO SEQUENT CALCULUS ⋮ Sequent calculi for semi-De Morgan and De Morgan algebras ⋮ Tautology Elimination, Cut Elimination, and S5 ⋮ General-elimination harmony and the meaning of the logical constants ⋮ A proof-search procedure for intuitionistic propositional logic ⋮ AN ANALYSIS OF THE RULES OF GENTZEN’SNJANDLJ ⋮ Does the deduction theorem fail for modal logic? ⋮ Socratic trees ⋮ Essential structure of proofs as a measure of complexity ⋮ Interpolation in extensions of first-order logic ⋮ A simple sequent calculus for Angell's logic of analytic containment ⋮ Metainferential reasoning on strong Kleene models ⋮ Disentangling structural connectives or life without display property ⋮ Dual erotetic calculi and the minimal \(\mathsf{LFI}\) ⋮ Herzberger's limit rule with labelled sequent calculus ⋮ Implications-as-rules vs. implications-as-links: an alternative implication-left schema for the sequent calculus ⋮ The original sin of proof-theoretic semantics ⋮ Free of Detachment: Logic, Rationality, and Gluts ⋮ Hypersequent calculi for intuitionistic logic with classical atoms ⋮ Negation-free and contradiction-free proof of the Steiner-Lehmus theorem ⋮ Proof-theoretic harmony: towards an intensional account ⋮ Two-sided sequent calculi for \textit{FDE}-like four-valued logics ⋮ Neutral free logic: motivation, proof theory and models ⋮ Proof theory for functional modal logic ⋮ Paradox and logical revision. A short introduction ⋮ Stanisław Jaśkowski and Natural Deduction Systems ⋮ Reasoning processes in propositional logic ⋮ The Church-Fitch knowability paradox in the light of structural proof theory ⋮ Reasoning about collectively accepted group beliefs ⋮ Focusing in Linear Meta-logic ⋮ Eliminability of cut in hypersequent calculi for some modal logics of linear frames ⋮ \(LE^{t}_{ \to }, LR^{ \circ }_{\widehat{\sim}}, LK\) and cutfree proofs ⋮ Proof analysis in intermediate logics ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017 ⋮ Composition of deductions within the propositions-as-types paradigm ⋮ Sufficient conditions for cut elimination with complexity analysis ⋮ Verificationism and Classical Realizability ⋮ Machine-Checked Proof-Theory for Propositional Modal Logics ⋮ Restricting Initial Sequents: The Trade-Offs Between Identity, Contraction and Cut ⋮ Sequent calculi for intuitionistic Gödel-Löb logic ⋮ Proof theory for heterogeneous logic combining formulas and diagrams: proof normalization ⋮ Towards a non-classical meta-theory for substructural approaches to paradox ⋮ Free logics are cut-free ⋮ On harmony and permuting conversions ⋮ General-elimination stability ⋮ Proofs and countermodels in non-classical logics ⋮ Axiomatizing geometric constructions ⋮ Reasoning about truth in first-order logic ⋮ Normal proofs, cut free derivations and structural rules ⋮ A survey of nonstandard sequent calculi ⋮ Decision methods for linearly ordered Heyting algebras ⋮ A framework for proof systems ⋮ A loop-free decision procedure for modal propositional logics K4, S4 and S5 ⋮ Recapturing dynamic logic of relation changers via bounded morphisms ⋮ A conservative negation extension of positive semilattice logic without the finite model property ⋮ Corrected upper bounds for free-cut elimination ⋮ Proof Theory for Distributed Knowledge ⋮ Translations between Gentzen-Prawitz and Jaśkowski-Fitch natural deduction proofs ⋮ Principles for object-linguistic consequence: from logical to irreflexive ⋮ Tableaux and dual tableaux: transformation of proofs ⋮ A message-passing interpretation of adjoint logic ⋮ Reasoning with ambiguity ⋮ Subatomic negation ⋮ What is the meaning of proofs?. A Fregean distinction in proof-theoretic semantics ⋮ On paradoxes in normal form ⋮ The bounded proof property via step algebras and step frames ⋮ Noncontractive classical logic ⋮ Proof-theoretic analysis of the logics of agency: the deliberative STIT ⋮ Subformula linking for intuitionistic logic with application to type theory ⋮ Classical harmony and separability ⋮ PROOF SYSTEMS FOR VARIOUS FDE-BASED MODAL LOGICS ⋮ FRACTIONAL SEMANTICS FOR CLASSICAL LOGIC ⋮ Normality, non-contamination and logical depth in classical natural deduction ⋮ Absorbing the structural rules in the sequent calculus with additional atomic rules ⋮ Cut elimination for entailment relations ⋮ Proof theory of Nelson's paraconsistent logic: a uniform perspective ⋮ Forms of the Pasch axiom in ordered geometry ⋮ Eight inference rules for implication ⋮ Maximum segments as natural deduction images of some cuts ⋮ Does the Implication Elimination Rule Need a Minor Premise? ⋮ Lyndon interpolation theorem of instantial neighborhood logic-constructively via a sequent calculus ⋮ A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems ⋮ Leśniewski's ontology -- proof-theoretic characterization ⋮ On the proof theory of infinitary modal logic ⋮ Modular sequent calculi for classical modal logics ⋮ Proof analysis in modal logic ⋮ Incomplete symbols -- definite descriptions revisited ⋮ Normalisation and subformula property for a system of classical logic with Tarski's rule

Uses Software

Pesca