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)

Cites work

• 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?)
• 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
• 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 Taming of the Cut. Classical Refutations with Analytic Cut
• The semantics and proof theory of linear logic

Cited in

(16)

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

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)