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

DOI10.1007/BF00881958zbMath0816.03012OpenAlexW2037991894MaRDI QIDQ1344886

Marcello D'Agostino, Dov M. 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)

Related Items

The universe of propositional approximations ⋮ 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 ⋮ The Universe of Approximations ⋮ Representing scope in intuitionistic deductions ⋮ Truth-values as labels: a general recipe for labelled deduction ⋮ Proof-search in type-theoretic languages: An introduction ⋮ Relational semantics and a relational proof system for full Lambek calculus ⋮ Using tableaux to automate the Lambek and other categorial calculi

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Simple consequence relations
• Proof methods for modal and intuitionistic logics
• The semantics and proof theory of linear logic
• Sequent-systems and groupoid models. I
• Relevant analytic tableaux
• Sequent-systems and groupoid models. II
• Are tableaux an improvement on truth-tables? Cut-free proofs and bivalence
• Intuitive semantics for first-degree entailments and `coupled trees'
• A semantical analysis of implicational system I and of the first degree of entailment
• Kripke models for linear logic
• Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic
• Decidability results in non-classical logics
• The Taming of the Cut. Classical Refutations with Analytic Cut
• Semantics for relevant logics