Results found: 2

Search results

Search:
in the keywords: hypersequent calculi

Sort By:

Limit search:

Hypersequent Calculi for S5: The Methods of Cut Elimination

100%

Bednarska K., Indrzejczak A.

Logic and Logical Philosophy

2015

vol. 24

issue 3

277–311

S5 is one of the most important modal logic with nice syntactic, semantic and algebraic properties. In spite of that, a successful (i.e. cut-free) formalization of S5 on the ground of standard sequent calculus (SC) was problematic and led to the invention of numerous nonstandard, generalized forms of SC. One of the most interesting framework which was very often used for this aim is that of hypersequent calculi (HC). The paper is a survey of HC for S5 proposed by Pottinger, Avron, Restall, Poggiolesi, Lahav and Kurokawa. We are particularly interested in examining different methods which were used for proving the eliminability/admissibility of cut in these systems and present our own variant of a system which admits relatively simple proof of cut elimination.

Simple cut elimination proof for hybrid logic

88%

Indrzejczak A.

Logic and Logical Philosophy

2016

vol. 25

issue 2

129–141

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.

Refine search results

2 Logic and Logical Philosophy

1 2016

1 2015

2 Indrzejczak A.

1 Bednarska K.

Search results

Hypersequent Calculi for S5: The Methods of Cut Elimination

Simple cut elimination proof for hybrid logic