A coding method for a sequent calculus of propositional logic

The paper deals with a coding method for a sequent calculus of the propositional logic. The method is based on the sequent calculus. It allows us to determine if a formula is derivable in the calculus without constructing a derivation tree. The main advantage of the coding method is its compactness in comparison with derivation trees of the sequent calculus. The coding method can be used as a decision procedure for the propositional logic.     

Sequent calculi for branching time temporal logics of knowledge and beliefwith awareness: Completeness and decidability

In this paper, we consider branching time temporal logic CT L with epistemic modalities for knowledge (belief) and with awareness operators. These logics involve the discrete-time linear temporal logic operators “next” and “until” with the branching temporal logic operator “on all paths”. In addition, the temporal logic of knowledge (belief) contains an indexed set of unary modal operators “agent i knows” (“agent i believes”). In a language of these logics, there are awareness operators. For these logics, we present sequent calculi with a restricted cut rule. Thus, we get proof systems where proof-search becomes decidable. The soundness and completeness for these calculi are proved. Published in Lietuvos Matematikos Rinkinys, Vol. 47, No. 3, pp. 328–340, July–September, 2007.     

On temporal logic S4Dbr

In this paper, we study the temporal logic S4Dbr with two temporal operators “always” and “eventually.” An equivalent sequent calculus is presented with formulae as modal clauses or modal clauses starting with operator “always.” An upper bound of deduction tree is given for propositional logic. A theorem prover for propositional logic is written in SWI-Prolog. Published in LietuvosMatematikos Rinkinys, Vol. 46, No. 2, pp. 203–214, April–June, 2006.     

A note on unbounded metric temporal logic over dense time domains

We investigate the consequences of removing the infinitary axiom and rules from a previously defined proof system for a fragment of propositional metric temporal logic over dense time (see [1]). (© 2006 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

Labeled sequent calculus for justification logics

Justification logics are modal-like logics that provide a framework for reasoning about justifications. This paper introduces labeled sequent calculi for justification logics, as well as for combined modal-justification logics. Using a method due to Sara Negri, we internalize the Kripke-style semantics of justification and modal-justification logics, known as Fitting models, within the syntax of the sequent calculus to produce labeled sequent calculi. We show that all rules of these systems are invertible and the structural rules (weakening and contraction) and the cut rule are admissible. Soundness and completeness are established as well. The analyticity for some of our labeled sequent calculi are shown by proving that they enjoy the subformula, sublabel and subterm properties. We also present an analytic labeled sequent calculus for $\mathsf{S4LPN}$ based on Artemov–Fitting models.     

Proof-theoretical investigation of temporal logic with time gaps

In the paper, the first-order intuitionistic temporal logic sequent calculus LBJ is considered. The invertibility of some of the LBJ rules, syntactic admissibility of the structural rules and the cut rule in LBJ, as well as Harrop and Craig's interpolation theorems for LBJ are proved. Gentzen's midsequent theorem is proved for the LBJ' calculus which is obtained from LBJ by removing the antecedent disjunction rule from it. Published in Lietuvos Matematikos Rinkinys, Vol. 40, No. 3, pp. 255–276, July–September, 2000.     

Some decidable classes of formulas of pure hybrid logic

We consider the formulas of pure hybrid logic without occurrences of a satisfaction operator. We describe a couple of formula derivation tactics in sequent calculus and prove the decidability of two classes of formulas. Decidable classes are obtained by setting restrictions on nominal occurrences in the formulas. Published in Lietuvos Matematikos Rinkinys, Vol. 44, No. 4, pp. 563–572, October–December, 2007.     

On a logic of involutive quantales

The logic just corresponding to (non‐commutative) involutive quantales, which was introduced by Wendy MacCaull, is reconsidered in order to obtain a cut‐free sequent calculus formulation, and the completeness theorem (with respect to the involutive quantale model ) for this logic is proved using a new admissible rule. (© 2005 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

Infinitary calculus for a restricted first-order linear temporal logic without contraction on quantified formulas

An infinitary calculus for a restricted fragment of the first-order linear temporal logic is considered. We prove that for this fragment one can construct the infinitary calculusG _Lω ^* without contraction on predicate formulas. The calculusG _Lω ^* possesses the following properties: (1) the succedent rule for the existential quantifier is included into the corresponding axiom; (2) the premise of the antecedent rule for the universal quantifier does not contain a duplicate of the main formula. The soundness and completness ofG _Lω ^* are also proved. Institute of Mathematics and Informatics, Akademijos 4, 2600 Vilnius, Lithuania. Translated from Lietuvos Matematikos Rinkinys, Vol. 39, No. 3, pp. 378–397, July–September, 1999. Translated by R. Lapinskas     

Sequent Calculi with Analytic Cut for Logics of Time and Knowledge with Perfect Recall

In this paper, we consider two logics of time and knowledge. These logics involve the discrete time linear temporal logic operators ``next' and ``until'. In addition, they contain an indexed set of unary epistemic modalities ``agent $i$ knows'. In these logics, the temporal and epistemic dimensions may interact. The particular interactions we consider capture perfect recall. We consider perfect recall in synchronously distributed systems and in systems without any assumptions. For these logics, we present sequent calculi with an analytic cut rule. Thus, we get proof systems where proof-search becomes decidable. The soundness and completeness of these calculi are proved.     

Sequent calculi for propositional star-free likelihood logic

We consider classical, multisuccedent intuitionistic, and intuitionistic sequent calculi for propositional likelihood logic. We prove the admissibility of structural rules and cut rule, invertibility of rules, correctness of the calculi, and completeness of the classical calculus with respect to given semantics.__________Published in Lietuvos Matematikos Rinkinys, Vol. 45, No. 1, pp. 3–21, January–March, 2005.     

Preservativity logic: An analogue of interpretability logic for constructive theories

In this paper we study the modal behavior of Σ‐preservativity, an extension of provability which is equivalent to interpretability for classical superarithmetical theories. We explain the connection between the principles of this logic and some well‐known properties of HA, like the disjunction property and its admissible rules. We show that the intuitionistic modal logic given by the preservativity principles of HA known so far, is complete with respect to a certain class of frames.     

Modal extension of ideal paraconsistent four-valued logic and its subsystem

This study aims to introduce a modal extension M4CC of Arieli, Avron, and Zamansky's ideal paraconsistent four-valued logic 4CC as a Gentzen-type sequent calculus and prove the Kripke-completeness and cut-elimination theorems for M4CC. The logic M4CC is also shown to be decidable and embeddable into the normal modal logic S4. Furthermore, a subsystem of M4CC, which has some characteristic properties that do not hold for M4CC, is introduced and the Kripke-completeness and cut-elimination theorems for this subsystem are proved. This subsystem is also shown to be decidable and embeddable into S4.     

Uniform interpolation and the existence of sequent calculi

This paper presents a uniform and modular method to prove uniform interpolation for several intermediate and intuitionistic modal logics. The proof-theoretic method uses sequent calculi that are extensions of the terminating sequent calculus $\mathsf{G4ip}$ for intuitionistic propositional logic. It is shown that whenever the rules in a calculus satisfy certain structural properties, the corresponding logic has uniform interpolation. It follows that the intuitionistic versions of $\mathsf{K}$ and $\mathsf{KD}$ (without the diamond operator) have uniform interpolation. It also follows that no intermediate or intuitionistic modal logic without uniform interpolation has a sequent calculus satisfying those structural properties, thereby establishing that except for the seven intermediate logics that have uniform interpolation, no intermediate logic has such a sequent calculus.     

A Sequent Calculus for Propositional Dynamic Logic for Agents

We consider propositional dynamic logic for agents. For this logic, we present a sequent calculus with a restricted cut rule and prove the soundness and completeness for the calculus.     

Efficient loop-check for KD 45 logic

We introduce a new sequent calculus for KD 45 logic. A loop-check technique is used to determine whether a sequent derivable or not. We concentrate ourselves on the efficiency of the loop-check technique used. The efficiency is obtained by making the loop-check to act locally (then we need to check only one or two current sequents), instead of a global loop-check used in known works as [3]. Moreover, the sequent calculus introduced uses a marked operator □ to integrate loop-check into an inference rule. Besides the efficient loop-check used, the sequent calculus introduced produces smaller derivation trees that reduce the derivation time. We also prove a lemma which determines the maximal number of modality rule applications in one branch of a tree. Published in Lietuvos Matematikos Rinkinys, Vol. 46, No. 1, pp. 55–66, January–March, 2006.     

A Sequent Calculus for Propositional Dynamic Logic for Agents with Interactions

We consider a propositional dynamic logic for agents with interactions such as known commitment, no learning, and perfect recall. For this logic, we present a sequent calculus with a restricted cut rule and prove the soundness and completeness for the calculus.__________Published in Lietuvos Matematikos Rinkinys, Vol. 45, No. 2, pp. 261–269, April–June, 2005.     

Glivenko Classes of Sequents for Temporal Logic with Time Gaps

Let LB be a sequent calculus of the first-order classical temporal logic TB with time gaps. Let, further, LBJ be the intuitionistic counterpart of LB. In this paper, we consider conditions under which a sequent is derivable in the calculus LBJ if and only if it is derivable in the calculus LB. Such conditions are defined for sequents with one formula in the succedent (purely Glivenko -classes) and for sequents with the empty succedent (Glivenko -classes).