A generalization of analytic deduction via labelled deductive systems. I: Basic substructural logics
From MaRDI portal
Publication:1344886
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
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
