Citations of:
Add citations
You must login to add citations.


A complete axiomatic system CTL$_{rp}$ is introduced for a temporal logic for finitely branching $\omega^+$trees in a temporal language extended with so called reference pointers. Syntactic and semantic interpretations are constructed for the branching time computation tree logic CTL* into CTL$_{rp}$. In particular, that yields a complete axiomatization for the translations of all valid CTL*formulae. Thus, the temporal logic with reference pointers is brought forward as a simpler (with no path quantifiers), but in a way more expressive medium for reasoning (...) 

We show that basic hybridization makes it possible to give straightforward Henkinstyle completeness proofs even when the modal logic being hybridized is higherorder. The key ideas are to add nominals as expressions of type t, and to extend to arbitrary types the way we interpret \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{69pt} \begin{document}$@_i$\end{document} in propositional and firstorder hybrid logic. This means: interpret \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{69pt} \begin{document}$@_i\alpha _a$\end{document}, where \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} (...) 

Reformulation strategies for solving Fitch’s paradox of knowability date back to Edgington. Their core assumption is that the formula \, from which the paradox originates, does not correctly express the intended meaning of the verification thesis, which should concern possible knowledge of actual truths, and therefore the contradiction does not represent a logical refutation of verificationism. Supporters of these solutions claim that can be reformulated in a way that blocks the derivation of the paradox. Unfortunately, these reformulation proposals come with (...) 

The paper introduces a firstorder theory in the language of predicate tense logic which contains a single simple axiom. It is shewn that this theory enables times to be referred to and sentences involving ‘now’ and ‘then’ to be formalised. The paper then compares this way of increasing the expressive capacity of predicate tense logic with other mechanisms, and indicates how to generalise the results to other modal and tense systems. 

In this paper we argue that hybrid logic is the deductive setting most natural for Kripke semantics. We do so by investigating hybrid axiomatics for a variety of systems, ranging from the basic hybrid language to the strong Priorean language . We show that hybrid logic offers a genuinely firstorder perspective on Kripke semantics: it is possible to define base logics which extend automatically to a wide variety of frame classes and to prove completeness using the Henkin method. In the (...) 

We consider the model checking problem for Hybrid Logic. Known algorithms so far are global in the sense that they compute, inductively, in every step the set of all worlds of a Kripke structure that satisfy a subformula of the input. Hence, they always exploit the entire structure. Local model checking tries to avoid this by only traversing necessary parts of the input in order to establish or refute the satisfaction relation between a given world and a formula. We present (...) 

We show that basic hybridization (adding nominals and @ operators) makes it possible to give straightforward Henkinstyle completeness proofs even when the modal logic being hybridized is higherorder. The key ideas are to add nominals as expressions of type t, and to extend to arbitrary types the way we interpret $@_i$ in propositional and firstorder hybrid logic. This means: interpret $@_i\alpha _a$ , where $\alpha _a$ is an expression of any type $a$ , as an expression of type $a$ that (...) 

Hybrid languages have both modal and firstorder characteristics: a Kripke semantics, and explicit variable binding apparatus. This paper motivates the development of hybrid languages, sketches their history, and examines the expressive power of three hybrid binders. We show that all three binders give rise to languages strictly weaker than the corresponding firstorder language, that full firstorder expressivity can be gained by adding the universal modality, and that all three binders can force the existence of infinite models and have undecidable satisfiability (...) 

This paper examines and classifies the computational complexity of model checking and satisfiability for hybrid logics over frames with equivalence relations. The considered languages contain all possible combinations of the downarrow binder, the existential binder, the satisfaction operator, and the global modality, ranging from the minimal hybrid language to very expressive languages. For model checking, we separate polynomialtime solvable from PSPACEcomplete cases, and for satisfiability, we exhibit cases complete for NP, PS pace , NE xp T ime , and even (...) 







Quantified hybrid logic is quantified modal logic extended with apparatus for naming states and asserting that a formula is true at a named state. While interpolation and Beth's definability theorem fail in a number of wellknown quantified modal logics , their counterparts in quantified hybrid logic have these properties. These are special cases of the main result of the paper: the quantified hybrid logic of any class of frames definable in the bounded fragment of firstorder logic has the interpolation property, (...) 

Hybrid languages are expansions of propositional modal languages which can refer to worlds. The use of strong hybrid languages dates back to at least [Pri67], but recent work has focussed on a more constrained system called $\mathscr{H}$. We show in detail that $\mathscr{H}$ is modally natural. We begin by studying its expressivity, and provide model theoretic characterizations and a syntactic characterization. The key result to emerge is that $\mathscr{H}$ corresponds to the fragment of firstorder logic which is invariant for generated (...) 

A complete axiomatic system CTL$_{rp}$ is introduced for a temporal logic for finitely branching $\omega^+$trees in a temporal language extended with so called reference pointers. Syntactic and semantic interpretations are constructed for the branching time computation tree logic CTL$^{*}$ into CTL$_{rp}$. In particular, that yields a complete axiomatization for the translations of all valid CTL$^{*}$formulae. Thus, the temporal logic with reference pointers is brought forward as a simpler (with no path quantifiers), but in a way more expressive medium for reasoning (...) 

