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.     

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.     

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.     

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

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.     

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

A multisymplectic framework for classical field theory and the calculus of variations II: space + time decomposition

In a previous paper I laid the foundations of a covariant Hamiltonian framework for the calculus of variations in general. The purpose of the present work is to demonstrate, in the context of classical field theory, how this covariant Hamiltonian formalism may be space + time decomposed. It turns out that the resulting “instantaneous” Hamiltonian formalism is an infinite- dimensional version of Ostrogradski 's theory and leads to the standard symplectic formulation of the initial value problem. The salient features of the analysis are: (i) the instantaneous Hamiltonian formalism does not depend upon the choice of Lepagean equivalent; (ii) the space + time decomposition can be performed either before or after the covariant Legendre transformation has been carried out, with equivalent results; (iii) the instantaneous Hamiltonian can be recovered in natural way from the multisymplectic structure inherent in the theory; and (iv) the space + time split symplectic structure lives on the space of Cauchy data for the evolution equations, as opposed to the space of solutions thereof.     

A simple logic for reasoning about incomplete knowledge

The semantics of modal logics for reasoning about belief or knowledge is often described in terms of accessibility relations, which is too expressive to account for mere epistemic states of an agent. This paper proposes a simple logic whose atoms express epistemic attitudes about formulae expressed in another basic propositional language, and that allows for conjunctions, disjunctions and negations of belief or knowledge statements. It allows an agent to reason about what is known about the beliefs held by another agent. This simple epistemic logic borrows its syntax and axioms from the modal logic KD. It uses only a fragment of the S5 language, which makes it a two-tiered propositional logic rather than as an extension thereof. Its semantics is given in terms of epistemic states understood as subsets of mutually exclusive propositional interpretations. Our approach offers a logical grounding to uncertainty theories like possibility theory and belief functions. In fact, we define the most basic logic for possibility theory as shown by a completeness proof that does not rely on accessibility relations.     

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.     

Completeness of two systems of illative combinatory logic for first-order propositional and predicate calculus

Illative combinatory logic consists of the theory of combinators or lambda calculus extended by extra constants (and corresponding axioms and rules) intended to capture inference. The paper considers 4 systems of illative combinatory logic that are sound for first-order propositional and predicate calculus. The interpretation from ordinary logic into the illative systems can be done in two ways: following the propositions-as-types paradigm, in which derivations become combinators, or in a more direct way, in which derivations are not translated. Both translations are closely related in a canonical way. In a preceding paper, Barendregt, Bunder and Dekkers, 1993, we proved completeness of the two direct translations. In the present paper we prove completeness of the two indirect translations by showing that the corresponding illative systems are conservative over the two systems for the direct translations. In another version, DBB (1997), we shall give a more direct completeness proof. These papers fulfill the program of Church and Curry to base logic on a consistent system of -terms or combinators. Hitherto this program had failed because systems of ICL were either too weak (to provide a sound interpretation) or too strong (sometimes even inconsistent). Received: February 15, 1996     

A formalization of Sambins's normalization for GL

Sambin [6] proved the normalization theorem (Hauptsatz) for GL, the modal logic of provability, in a sequent calculus version called by him GLS. His proof does not take into account the concept of reduction, commonly used in normalization proofs. Bellini [1], on the other hand, gave a normalization proof for GL using reductions. Indeed, Sambin's proof is a decision procedure which builds cut-free proofs. In this work we formalize this procedure as a recursive function and prove its recursiveness in an arithmetically formalizable way, concluding that the normalization of GL can be formalized in PA. MSC: 03F05, 03B35, 03B45.     

Malliavin calculus for Markov chains using perturbations of time

In this article, we develop a Malliavin calculus associated to a time-continuous Markov chain with finite state space. We apply it to get a criterion of density for solutions of stochastic differential equation involving the Markov chain and also to compute greeks.