A generalization of analytic deduction via labelled deductive systems. I: Basic substructural logics

DOI10.1007/BF00881958MaRDI QIDQ1344886zbMATH OpenOpenAlexFDO

Authors Marcello D'Agostino, Dov Gabbay

Publication date 22 February 1995

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bf00881958

zbMATH Keywords

implicational propositional systems with restricted structural ruleslabelled deduction systems

Mathematics Subject Classification ID

Other nonclassical logic (03B60) Cut-elimination and normal-form theorems (03F05)

Review text

Several implicational propositional systems with restricted structural rules (for example linear and relevant implication) are presented in terms of labelled deduction systems introduced by the second author.

Cites work

• A semantical analysis of implicational system I and of the first degree of entailment
• Are tableaux an improvement on truth-tables? Cut-free proofs and bivalence
• Decidability results in non-classical logics
• scientific article; zbMATH DE number 46487 (Why is no real title available?)
• scientific article; zbMATH DE number 49746 (Why is no real title available?)
• scientific article; zbMATH DE number 3496100 (Why is no real title available?)
• scientific article; zbMATH DE number 3504935 (Why is no real title available?)
• scientific article; zbMATH DE number 517067 (Why is no real title available?)
• scientific article; zbMATH DE number 4117898 (Why is no real title available?)
• scientific article; zbMATH DE number 1406801 (Why is no real title available?)
• scientific article; zbMATH DE number 1406810 (Why is no real title available?)
• scientific article; zbMATH DE number 1406811 (Why is no real title available?)
• Intuitive semantics for first-degree entailments and `coupled trees'
• Kripke models for linear logic
• Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic
• Proof methods for modal and intuitionistic logics
• Relevant analytic tableaux
• Semantics for relevant logics
• Sequent-systems and groupoid models. I
• Sequent-systems and groupoid models. II
• Simple consequence relations
• The semantics and proof theory of linear logic
• The Taming of the Cut. Classical Refutations with Analytic Cut

Cited in

(17)

• Representing scope in intuitionistic deductions
• Proof-search in type-theoretic languages: An introduction
• Using tableaux to automate the Lambek and other categorial calculi
• The universe of propositional approximations
• Truth-values as labels: a general recipe for labelled deduction
• Relational semantics and a relational proof system for full Lambek calculus
• scientific article; zbMATH DE number 510780 (Why is no real title available?)
• Labelling ideality and subideality
• Fibred tableaux for multi-implication logics
• Distributed modal theorem proving with KE
• Tableaux and algorithms for Propositional Dynamic Logic with Converse
• Grammar specification in categorial logics and theorem proving
• scientific article; zbMATH DE number 753774 (Why is no real title available?)
• scientific article; zbMATH DE number 2119403 (Why is no real title available?)
• scientific article; zbMATH DE number 822106 (Why is no real title available?)
• The universe of approximations
• Labelled KE for intuitionistic propositional logic

This page was built for publication: A generalization of analytic deduction via labelled deductive systems. I: Basic substructural logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1344886)