Search

In this paper, we focus on a logical approach to the important notion of closeness, which has not received much attention in the literature. Our notion of closeness is based on the so-called proximity intervals , which will be used to decide the elements that are close to each other. Some of the intuitions of this definition are explained on the basis of examples. We prove the decidability of the recently introduced multimodal logic for closeness and, then, we show some capabilities of the logic with respect to expressivity in order to denote particular positions of the proximity intervals. [ABSTRACT FROM AUTHOR]

Bull's theorem states that all axiomatic extensions of the modal logic S4.3 have the finite model property. We show that this fails for hybrid logic, by defining an axiomatic extension of the hybrid companion of S4.3, which has only infinite Kripke models. In contrast, by considering hybrid algebraic semantics or, dually, semantics based on two-sorted general frames, we are able to prove analogues of Bull's theorem for two hybrid languages. [ABSTRACT FROM AUTHOR]

The paper considers modal logics of products of neighbourhood frames. The n-product of modal logics is the logic of all products of neighbourhood frames of the corresponding logics. We find the n-product of any two pretransitive Horn axiomatizable logics. As a corollary, we find the d-logic of products of topological spaces from some classes of topological spaces. [ABSTRACT FROM AUTHOR]

We introduce a new Gentzen-style framework of grafted hypersequents that combines the formalism of nested sequents with that of hypersequents. To illustrate the potential of the framework, we present novel calculi for the modal logics K5 and KD5, as well as for extensions of the modal logics K and KD with the axiom for shift reflexivity. The latter of these extensions is also known as SDL+ in the context of deontic logic. All our calculi enjoy syntactic cut-elimination and can be used in backwards proof search procedures of optimal complexity. The tableaufication of the calculi for K5 and KD5 yields simplified prefixed tableau calculi for these logic reminiscent of the simplified tableau system for S5, which might be of independent interest. [ABSTRACT FROM AUTHOR]

Following a result by De Rijke for modal logic, it is shown that the basic weak entailment model-theoretic language with absurdity is the maximal model-theoretic language having (i) the finite occurrence property, (ii) preservation under relevant directed bisimulations and (iii) the finite depth property. This can be seen as a generalized preservation theorem characterizing propositional weak entailment formulas among formulas of other model-theoretic languages. [ABSTRACT FROM AUTHOR]

The celebrated theorem proved by Goldblatt and Thomason in 1974 gives necessary and sufficient conditions for an elementary class of Kripke frames to be modally definable. Here we obtain a local analogue of this result, which deals with modal definability of classes of pointed frames. Furthermore, we generalize it to the case of n-frames, which are frames with n distinguished worlds. For talking about n-frames, we generalize modal formulas to modal expressions. While a modal formula is evaluated at a single world of a model, a modal expression with n individual variables is evaluated at an n-tuple of worlds, just as a first-order formula with n free variables. We introduce operations on n-frames that preserve validity of modal expressions, and show that closure under these operations is a necessary and sufficient condition for an elementary class of n-frames to be modally definable. We also discuss the relationship between modal expressions and hybrid logic and leave open questions. [ABSTRACT FROM AUTHOR]

We study dynamic modal operators that can change the accessibility relation of a model during the evaluation of a formula. In particular, we extend the basic modal language with modalities that are able to delete, add or swap an edge between pairs of elements of the domain. We define a generic framework to characterize this kind of operations. First, we investigate relation-changing modal logics as fragments of classical logics. Then, we use the new framework to get a suitable notion of bisimulation for the logics introduced, and we investigate their expressive power. Finally, we show that the complexity of the model checking problem for the particular operators introduced is PSPACE-complete, and we study two subproblems of model checking: formula complexity and program complexity. [ABSTRACT FROM AUTHOR]

In this article, we discuss a well-known self-referential paradox in epistemic game theory, the Brandenburger–Keisler paradox. We approach the paradox from two different perspectives, non-well-founded set theory and paraconsistent logic, and provide models in which the paradox is solved. [ABSTRACT FROM AUTHOR]

We investigate dynamic modal operators that can change the model during evaluation. We define the logic SL by extending the basic modal language with the modality, which is a diamond operator that in addition has the ability to invert pairs of related elements in the domain while traversing an edge of the accessibility relation. SL is very expressive: it fails to have the finite and the tree model property. We show that SL is equivalent to a fragment of first-order logic by providing a satisfiability preserving translation. In addition, we provide an equivalence preserving translation from SL to the hybrid logic H(:,↓ ). We also define a suitable notion of bisimulation for SL and investigate its expressive power, showing that it lies strictly between the basic modal logic and H(:,↓ ). We finally show that its model checking problem is PSpace-complete and its satisfiability problem is undecidable. [ABSTRACT FROM PUBLISHER]

Hybrid logic is an extension of modal logic which allows us to refer explicitly to points of the model in the syntax of formulas. It is easy to justify interest in hybrid logic on applied grounds, with the usefulness of the additional expressive power. For example, when reasoning about time one often wants to build up a series of assertions about what happens at a particular instant, and standard modal formalisms do not allow this. What is less obvious is that the route hybrid logic takes to overcome this problem often actually improves the behaviour of the underlying modal formalism. For example, it becomes far simpler to formulate proof-systems for hybrid logic, and completeness results can be proved of a generality that is simply not available in modal logic. That is, hybridization is a systematic way of remedying a number of known deficiencies of modal logic. First-order hybrid logic is obtained by adding first-order machinery to propositional hybrid logic, or equivalently, by adding hybrid-logical machinery to first-order modal logic. In this short paper we introduce first-order hybrid logic and we give a survey of work in the area. [ABSTRACT FROM AUTHOR]

Graphs are among the most frequently used structures in Computer Science. Some of the properties that must be checked in many applications are connectivity, acyclicity and the Eulerian and Hamiltonian properties. In this work, we analyze how we can express these four properties with modal logics. This involves two issues: whether each of the modal languages under consideration has enough expressive power to describe these properties and how complex (computationally) it is to use these logics to actually test whether a given graph has some desired property. First, we show that these properties are not definable in a basic modal logic or in any bisimulation-invariant extension of it, like the modal μ-calculus. We then show that it is possible to express some of the above properties in a basic hybrid logic. Unfortunately, the Hamiltonian and Eulerian properties still cannot be efficiently checked. In a second attempt, we propose an extension of CTL* with nominals and show that the Hamiltonian property can be more efficiently checked in this logic than in the previous one. In a third attempt, we extend the basic hybrid logic with the ↓ operator and show that we can check the Hamiltonian property with optimal (NP) complexity in this logic. Finally, we tackle the Eulerian property in two different ways. First, we develop a generic method to express edge-related properties in hybrid logics and use it to express the Eulerian property. Second, we express a necessary and sufficient condition for the Eulerian property to hold using a graded modal logic. [ABSTRACT FROM PUBLISHER]