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.     

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.     

A Decision Procedure for Nonperiodic Sequents of the First-Order Linear Temporal Logic

A deduction-based decision procedure is presented for the nonperiodic D-sequents of the first-order linear temporal logic. The D-sequents are obtained from D ₂-sequents [7], [8] by removing the periodicity condition. The deductive procedure proposed consists of decidable deductive procedures that replace infinitary and finitary induction rules for the temporal operator ``always'. The soundness and completeness of the deduction-based decision procedure proposed is proved.     

Specialization of Loop Rules of a Sequent Calculus of Intuitionistic Temporal Logic with Time Gaps

The paper deals with the loop-rule problem in the first-order intuitionistic temporal logic sequent calculus LBJ. The calculus LBJT is intended for the specialization of the antecedent implication rule. The invertibility of some of the LBJT rules and the syntactic admissibility of the structural rules and the cut rule in LBJT, as well as the equivalence of LBJ and LBJT, are proved. The calculus LBJT2 is intended for the specialization of the antecedent universal quantifier and antecedent box rules. The decidability of LBJT2 is proved.     

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.     

New sequent calculi for Visser's Formal Propositional Logic

Two cut‐free sequent calculi which are conservative extensions of Visser's Formal Propositional Logic (FPL) are introduced. These satisfy a kind of subformula property and by this property the interpolation theorem for FPL are proved. These are analogies to Aghaei‐Ardeshir's calculi for Visser's Basic Propositional Logic.     

Dual‐Context Sequent Calculus and Strict Implication

We introduce a dual‐context style sequent calculus which is complete with respectto Kripke semantics where implication is interpreted as strict implication in the modal logic K. The cut‐elimination theorem for this calculus is proved by a variant of Gentzen's method.     

Sequent systems for compact bilinear logic

Compact Bilinear Logic (CBL), introduced by Lambek [14], arises from the multiplicative fragment of Noncommutative Linear Logic of Abrusci [1] (also called Bilinear Logic in [13]) by identifying times with par and 0 with 1. In this paper, we present two sequent systems for CBL and prove the cut‐elimination theorem for them. We also discuss a connection between cut‐elimination for CBL and the Switching Lemma from [14].     

A sequent calculus for logic of knowledge and past time: Completeness and decidability

We consider logic of knowledge and past time. This logic involves the discrete-time linear temporal operators next, until, weak yesterday, and since. In addition, it contains an indexed set of unary modal operators agent i knows.We consider the semantic constraint of the unique initial states for this logic. For the logic, we present a sequent calculus with a restricted cut rule. We prove the soundness and completeness of the sequent calculus presented. We prove the decidability of provability in the considered calculus as well. So, this calculus can be used as a basis for automated theorem proving. The proof method for the completeness can be used to construct complete sequent calculi with a restricted cut rule for this logic with other semantical constraints as well. Published in Lietuvos Matematikos Rinkinys, Vol. 46, No. 3, pp. 427–437, July–September, 2006.     

A secondary semantics for Second Order Intuitionistic Propositional Logic

In this paper we propose a Kripke‐style semantics for second order intuitionistic propositional logic and we provide a semantical proof of the disjunction and the explicit definability property. Moreover, we provide a tableau calculus which is sound and complete with respect to such a semantics. (© 2004 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

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).     

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.     

Infinitary Calculus without Loop Rules for Restricted Sequents of the First-Order Linear Temporal Logic

A restricted first-order linear temporal logic with temporal operators next and always is considered. We prove that for this logic one can construct a sequential calculus without loop rules, i.e., the rules containing a duplication of the main formula in the premises of these rules. This paper continues the previous work of the author, where an infinitary calculus without loop rules on the logical level, but containing the traditional loop antecedent rule for the operator always, was constructed. In this paper, in order to remove this loop rule we introduce a nonlocal rule allowing us to eliminate loops in the process of the proof search. The soundness and >-completeness of the constructed calculus is proved.     

Cut-Free Ordinary Sequent Calculi for Logics Having Generalized Finite-Valued Semantics

The paper presents a method for transforming a given sound and complete n-sequent proof system into an equivalent sound and complete system of ordinary sequents. The method is applicable to a large, central class of (generalized) finite-valued logics with the language satisfying a certain minimal expressiveness condition. The expressiveness condition decrees that the truth-value of any formula φ must be identifiable by determining whether certain formulas uniformly constructed from φ have designated values or not. The transformation preserves the general structure of proofs in the original calculus in a way ensuring preservation of the weak cut elimination theorem under the transformation. The described transformation metod is illustrated on several concrete examples of many-valued logics, including a new application to information sources logics.     

A Basis in Semi‐Reduced Form for the Admissible Rules of the Intuitionistic Logic IPC

We study the problem of finding a basis for all rules admissible in the intuitionistic propositional logic IPC. The main result is Theorem 3.1 which gives a basis consisting of all rules in semi‐reduced form satisfying certain specific additional requirements. Using developed technique we also find a basis for rules admissible in the logic of excluded middle law KC.