Full-text resources of CEJSH and other databases are now available in the new Library of Science.
Visit https://bibliotekanauki.pl

Results found: 4

first rewind previous Page / 1 next fast forward last

Search results

Search:
in the keywords:  sequent calculi
help Sort By:

help Limit search:
first rewind previous Page / 1 next fast forward last
1

Sequents for non-wellfounded mereology

100%
Maffezioli P.
Logic and Logical Philosophy
|
2016
|
vol. 25
|
issue 3 Mereology and Beyond (II)
351-369
EN
The paper explores the proof theory of non-wellfounded mereology with binary fusions and provides a cut-free sequent calculus equivalent to the standard axiomatic system.
2

Admissibility of Cut in Congruent Modal Logics

100%
Indrzejczak A.
Logic and Logical Philosophy
|
2011
|
vol. 20
|
issue 3
189-203
EN
We present a detailed proof of the admissibility of cut in sequent calculus for some congruent modal logics. The result was announced much earlier during the Trends in Logic Conference, Toruń 2006 and the proof for monotonic modal logics was provided already in Indrzejczak [5]. Also some tableau and natural deduction formalizations presented in Indrzejczak [6] and Indrzejczak [7] were based on this result but the proof itself was not published so far. In this paper we are going to fill this gap. The delay was partly due to the fact that the author from time to time was trying to improve the result and extend it to some additional logics by testing other methods of proving cut elimination. Unfortunately all these attempts failed and cut elimination holds only for these logics which were proved to satisfy this property already in 2005.
3
Content available remote

Simple cut elimination proof for hybrid logic

88%
Indrzejczak A.
Logic and Logical Philosophy
|
2016
|
vol. 25
|
issue 2
129–141
EN
In the paper we present a relatively simple proof of cut elimination theorem for variety of hybrid logics in the language with satisfaction operators and universal modality. The proof is based on the strategy introduced originally in the framework of hypersequent calculi but it works well also for standard sequent calculi. Sequent calculus examined in the paper works on so called satisfaction formulae and cover all logics adequate with respect to classes of frames defined by so called geometric conditions.
4

Decision procedures for some strong hybrid logics

75%
Indrzejczak A., Zawidzki M.
Logic and Logical Philosophy
|
2013
|
vol. 22
|
issue 4
389-409
EN
Hybrid logics are extensions of standard modal logics, which significantly increase the expressive power of the latter. Since most of hybrid logics are known to be decidable, decision procedures for them is a widely investigated field of research. So far, several tableau calculi for hybrid logics have been presented in the literature. In this paper we introduce a sound, complete and terminating tableau calculus TH(@,E,D,♦ −) for hybrid logics with the satisfaction operators, the universal modality, the difference modality and the inverse modality as well as the corresponding sequent calculus SH(@,E,D,♦ −). They not only uniformly cover relatively wide range of various hybrid logics but they are also conceptually simple and enable effective search for a minimal model for a satisfiable formula. The main novelty is the exploitation of the unrestricted blocking mechanism introduced as an explicit, sound tableau rule.
first rewind previous Page / 1 next fast forward last
JavaScript is turned off in your web browser. Turn it on to take full advantage of this site, then refresh the page.