On the Tree-Hypersequent Calculi

2010 ◽  
pp. 119-141 ◽  
Author(s):  
Francesca Poggiolesi
Keyword(s):  
Hypersequent Calculi

scholarly journals Bunched Hypersequent Calculi for Distributive Substructural Logics

10.29007/ngp3 ◽  
2018 ◽  
Author(s):  
Agata Ciabattoni ◽  
Revantha Ramanayake
Keyword(s):  
Large Class ◽  
General Rule ◽  
Expressive Power ◽  
Substructural Logics ◽  
Cut Elimination ◽  
Lambek Calculus ◽  
Hypersequent Calculi

We introduce a new proof-theoretic framework which enhances the expressive power of bunched sequents by extending them with a hypersequent structure. A general cut-elimination theorem that applies to bunched hypersequent calculi satisfying general rule conditions is then proved. We adapt the methods of transforming axioms into rules to provide cutfree bunched hypersequent calculi for a large class of logics extending the distributive commutative Full Lambek calculus DFLe and Bunched Implication logic BI. The methodology is then used to formulate new logics equipped with a cutfree calculus in the vicinity of Boolean BI.

scholarly journals Cut Elimination Theorem for Non-Commutative Hypersequent Calculus

2017 ◽  
Vol 46 (1/2) ◽  
Author(s):  
Andrzej Indrzejczak
Keyword(s):  
Temporal Logic ◽  
Cut Elimination ◽  
Temporal Logics ◽  
Hypersequent Calculi ◽  
Flow Of Time

Hypersequent calculi (HC) can formalize various non-classical logics. In [9] we presented a non-commutative variant of HC for the weakest temporal logic of linear frames Kt4.3 and some its extensions for dense and serial flow of time. The system was proved to be cut-free HC formalization of respective temporal logics by means of Schütte/Hintikka-style semantical argument using models built from saturated hypersequents. In this paper we present a variant of this calculus for Kt4.3 with a constructive syntactical proof of cut elimination.

scholarly journals Sequent and hypersequent calculi for abelian and łukasiewicz logics

2005 ◽  
Vol 6 (3) ◽  
pp. 578-613 ◽  
Author(s):  
George Metcalfe ◽  
Nicola Olivetti ◽  
Dov Gabbay
Keyword(s):  
Hypersequent Calculi ◽  
Łukasiewicz Logics

scholarly journals Hypersequent calculi for non-normal modal and deontic logics: countermodels and optimal complexity

2020 ◽  
Author(s):  
Tiziano Dalmonte ◽  
Björn Lellmann ◽  
Nicola Olivetti ◽  
Elaine Pimentel
Keyword(s):  
Search Strategy ◽  
Cut Elimination ◽  
Relational Semantics ◽  
Optimal Complexity ◽  
Proof Search ◽  
Polynomial Size ◽  
Hypersequent Calculi

Abstract We present some hypersequent calculi for all systems of the classical cube and their extensions with axioms ${T}$, ${P}$ and ${D}$ and for every $n \geq 1$, rule ${RD}_n^+$. The calculi are internal as they only employ the language of the logic, plus additional structural connectives. We show that the calculi are complete with respect to the corresponding axiomatization by a syntactic proof of cut elimination. Then, we define a terminating proof search strategy in the hypersequent calculi and show that it is optimal for coNP-complete logics. Moreover, we show that from every failed proof of a formula or hypersequent it is possible to directly extract a countermodel of it in the bi-neighbourhood semantics of polynomial size for coNP logics, and for regular logics also in the relational semantics. We finish the paper by giving a translation between hypersequent rule applications and derivations in a labelled system for the classical cube.

Sign in / Sign up

Export Citation Format

Share Document