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.     

Sémantique algébrique ďun système logique basé sur un ensemble ordonné fini

In order to modelize the reasoning of an intelligent agent represented by a poset T, H. Rasiowa introduced logic systems called “Approximation Logics”. In these systems a set of constants constitutes a fundamental tool. In this papers, we consider logic systems called L′_T without this kind of constants but limited to the case where T is a finite poset. We prove a weak deduction theorem. We introduce also an algebraic semantics using Hey ting algebra with operators. To prove the completeness theorem of the L′_T system with respect to the algebraic semantics, we use the method of H. Rasiowa and R. Sikorski for first order logic. In the propositional case, a corollary allows us to assert that it is decidable to know “if a propositional formula is valid”. We study also certain relations between the L′_T logic and the intuitionistic and classical logics.     

Koplienko–Neidhardt trace formula for pairs of contraction operators and pairs of maximal dissipative operators

We present a generalization of Koplienko–Neidhardt trace formula for pairs of Hilbert space operators (T , V ) with T contractive and V unitary such that T – V is a Hilbert–Schmidt operator. We extend the result to pairs of contractions and then, via Cayley transform, to pairs of maximal dissipative operators. (© 2006 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

A Note on a Class of Operators

The aim of this note is to study the spectral properties of the LUECKE's class R of operators T such that ‖(T – zI)^?1‖=1/d(z, W(T)) for all z?CLW(T), where CLW(T) is the closure of the numerical range W(T) of T and d(z, W(T)) is the distance from z to W(T). The main emphasis is on the investigation of those properties of operators of class R which are either similar to or distinct from those of operators satisfying the growth condition (G₁).     

Modal operators on bounded commutative residuated <Emphasis Type="Italic">ℓ</Emphasis>-monoids

Bounded commutative residuated lattice ordered monoids (Rℓ-monoids) are a common generalization of, e.g., Heyting algebras and BL-algebras, i.e., algebras of intuitionistic logic and basic fuzzy logic, respectively. Modal operators (special cases of closure operators) on Heyting algebras were studied in [MacNAB, D. S.: Modal operators on Heyting algebras, Algebra Universalis 12 (1981), 5–29] and on MV-algebras in [HARLENDEROVá,M.—RACHŮNEK, J.: Modal operators on MV-algebras, Math. Bohem. 131 (2006), 39–48]. In the paper we generalize the notion of a modal operator for general bounded commutative Rℓ-monoids and investigate their properties also for certain derived algebras. The first author was supported by the Council of Czech Government, MSM 6198959214.     

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.     

BV ‐extension of rate independent operators

Rate independent operators naturally arise in the mathematical analysis of hysteresis. Among rate independent operators, the locally monotone ones are those better suited for the study of PDE's with hysteresis. We prove that a rate independent operator R: Lip (0, T) → BV (0, T) ∩ C (0, T) which is locally monotone and continuous with respect to the strict topology of BV admits a unique continuous extension R?: BV (0, T) → BV (0, T). This general result applies to several concrete hysteresis operators. For many of these operators the existence of a continuous extension was previously known at most to the space BV (0, T) ∩ C (0, T). (© 2009 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

A Modal Logic That is Complete with Respect to Strictly Linearly Ordered <Emphasis Type="Italic">A</Emphasis>-Models

An axiomatization is furnished for a polymodal logic of strictly linearly ordered A-frames: for frames of this kind, we consider a language of polymodal logic with two modal operators, □_< and □_≺. In the language, along with the operators, we introduce a constant β, which describes a basis subset. In the language with the two modal operators and constant β, an Lα-calculus is constructed. It is proved that such is complete w.r.t. the class of all strictly linearly ordered A-frames. Moreover, it turns out that the calculus in question possesses the finite-model property and, consequently, is decidable. __________ Translated from Algebra i Logika, Vol. 44, No. 5, pp. 560–582, September–October, 2005. Supported by RFBR grant No. 03-06-80178, by the Council for Grants (under RF President) and State Aid of Fundamental Science Schools, project NSh-2069.2003.1, and by INTAS grant No. 04-77-7080.     

On non‐compact logics in NEXT(KTB)

In this paper we construct a continuum of logics, extensions of the modal logic T₂ = KTB ⊕ □²p → □³p, which are non‐compact (relative to Kripke frames) and hence Kripke incomplete. (© 2008 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

The modal logic of the countable random frame

 We study the modal logic M L ^r of the countable random frame, which is contained in and `approximates' the modal logic of almost sure frame validity, i.e. the logic of those modal principles which are valid with asymptotic probability 1 in a randomly chosen finite frame. We give a sound and complete axiomatization of M L ^r and show that it is not finitely axiomatizable. Then we describe the finite frames of that logic and show that it has the finite frame property and its satisfiability problem is in EXPTIME. All these results easily extend to temporal and other multi-modal logics. Finally, we show that there are modal formulas which are almost surely valid in the finite, yet fail in the countable random frame, and hence do not follow from the extension axioms. Therefore the analog of Fagin's transfer theorem for almost sure validity in first-order logic fails for modal logic. Received: 1 May 2000 / Revised version: 29 July 2001 / Published online: 2 September 2002 Mathematics Subject Classification (2000): 03B45, 03B70, 03C99 Key words or phrases: Modal logic – Random frames – Almost sure frame validity – Countable random frame – Axiomatization – Completeness     

Interpolation properties in the extensions of the logic of inequality

We consider the modal logics wK4 and DL as well as the corresponding weakly transitive modal algebras and DL-algebras. We prove that there exist precisely 16 amalgamable varieties of DL-algebras. We find a criterion for the weak amalgamation property of varieties of weakly transitive modal algebras, solve the deductive interpolation problem for extensions of the logic of inequality DL, and obtain a weak interpolation criterion over wK4.     

Barwise's information frames and modal logics

 The paper studies Barwise's information frames and answers the John Barwise question: to find axiomatizations for the modal logics generated by information frames. We find axiomatic systems for (i) the modal logic of all complete information frames, (ii) the logic of all sound and complete information frames, (iii) the logic of all hereditary and complete information frames, (iv) the logic of all complete, sound and hereditary information frames, and (v) the logic of all consistent and complete information frames. The notion of weak modal logics is also proposed, and it is shown that the weak modal logics generated by all information frames and by all hereditary information frames are K and K4 respectively. To develop general theory, we prove that (i) any Kripke complete modal logic is the modal logic of a certain class of information frames and that (ii) the modal logic generated by any given class of complete, rarefied and fully classified information frames is Kripke complete. This paper is dedicated to the memory of talented mathematician John Barwise. Received: 7 May 2000 Published online: 10 October 2002 Key words or phrases: Knowledge presentation – Information – Information flow – Information frames – Modal logic-Kripke model     

Sémantique de type Kripke d'un système logique basé sur un ensemble ordonné fini

In order to modelize the reasoning of intelligent agents represented by a poset T, H. Rasiowa introduced logic systems called “Approximation Logics”. In these systems the use of a set of constants constitutes a fundamental tool. We have introduced in [8] a logic system called without this kind of constants but limited to the case that T is a finite poset. We have proved a completeness result for this system w.r.t. an algebraic semantics. We introduce in this paper a Kripke‐style semantics for a subsystem of for which there existes a deduction theorem. The set of “possible worldsr is enriched by a family of functions indexed by the elements of T and satisfying some conditions. We prove a completeness result for system with respect to this Kripke semantics and define a finite Kripke structure that characterizes the propositional fragment of logic . We introduce a reational semantics (found by E. Orlowska) which has the advantage to allow an interpretation of the propositionnal logic using only binary relations. We treat also the computational complexity of the satisfiability problem of the propositional fragment of logic .     

On Ideal Operators

Let E, F be Archimedean Riesz spaces. We consider operators that map ideals of E to ideals of F and operators T for which, T ^–1 (I) is an ideal in E, for each ideal I in F. We study the properties of such operators and investigate their relation to disjointness preserving operators.     

Mixed logic and storage operators

In 1990 J-L. Krivine introduced the notion of storage operators. They are -terms which simulate call-by-value in the call-by-name strategy and they can be used in order to modelize assignment instructions. J-L. Krivine has shown that there is a very simple second order type in AF2 type system for storage operators using G?del translation of classical to intuitionistic logic. In order to modelize the control operators, J-L. Krivine has extended the system AF2 to the classical logic. In his system the property of the unicity of integers representation is lost, but he has shown that storage operators typable in the system AF2 can be used to find the values of classical integers. In this paper, we present a new classical type system based on a logical system called mixed logic. We prove that in this system we can characterize, by types, the storage operators and the control operators. Received: 7 May 1997     

A Geometrical Look at Iterative Methods for Operators with Fixed Points

ABSTRACT

We distinguish classes of operators T with fixed points on a real Hilbert space by comparing the distances of a point x and its image Tx to the (set of) fixed points of T; this leads to a ranking of those classes, based on a nonnegative parameter. That same parameter also lets us conclude about the sign of and an upper bound for a characteristic inner product result that arises in iterative processes to obtain a common fixed point of a set of operators. We use that parameter as the starting point for a geometrically-inclined study of specific iterative algorithms intended to find a common fixed point of operators belonging to such class.     

Discrete Quantum Scattering Theory

We formulate quantum scattering theory in terms of a discrete L ₂-basis of eigen differentials. Using projection operators in the Hilbert space, we develop a universal method for constructing finite-dimensional analogues of the basic operators of the scattering theory: S- and T-matrices, resolvent operators, and Möller wave operators as well as the analogues of resolvent identities and the Lippmann–Schwinger equations for the T-matrix. The developed general formalism of the discrete scattering theory results in a very simple calculation scheme for a broad class of interaction operators.     

Localized SVEP, Property (b) and Property (ab)

Property (b) for a bounded linear operator ${T \in L(X)}$ on a Banach space X means that the points λ of the approximate point spectrum for which λI – T is upper semi-Weyl are exactly the spectral points λ for which λI – T is Browder. In this paper we shall give several characterizations of operators T for which T, or its dual T*, has property (b). We also investigate the property (ab) which is closely related to property (b).     

Logical Extensions of Aristotle’s Square

We start from the geometrical-logical extension of Aristotle’s square in [6,15] and [14], and study them from both syntactic and semantic points of view. Recall that Aristotle’s square under its modal form has the following four vertices: A is □α, E is , I is and O is , where α is a logical formula and □ is a modality which can be defined axiomatically within a particular logic known as S5 (classical or intuitionistic, depending on whether is involutive or not) modal logic. [3] has proposed extensions which can be interpreted respectively within paraconsistent and paracomplete logical frameworks. [15] has shown that these extensions are subfigures of a tetraicosahedron whose vertices are actually obtained by closure of by the logical operations , under the assumption of classical S5 modal logic. We pursue these researches on the geometrical-logical extensions of Aristotle’s square: first we list all modal squares of opposition. We show that if the vertices of that geometrical figure are logical formulae and if the sub-alternation edges are interpreted as logical implication relations, then the underlying logic is none other than classical logic. Then we consider a higher-order extension introduced by [14], and we show that the same tetraicosahedron plays a key role when additional modal operators are introduced. Finally we discuss the relation between the logic underlying these extensions and the resulting geometrical-logical figures.      

On the Property (gw)

In this note we introduce and study the property (gw), which extends property (w) introduced by Rakoc̆evic in [23]. We investigate the property (gw) in connection with Weyl type theorems. We show that if T is a bounded linear operator T acting on a Banach space X, then property (gw) holds for T if and only if property (w) holds for T and Π _a (T) = E(T), where Π _a (T) is the set of left poles of T and E(T) is the set of isolated eigenvalues of T. We also study the property (gw) for operators satisfying the single valued extension property (SVEP). Classes of operators are considered as illustrating examples. The second author was supported by Protars D11/16 and PGR- UMP.