1,721,264 research outputs found
A Road Map of Interval Temporal Logics and Duration Calculi
Full text linkWe survey main developments, results, and open problems on interval temporal logics and duration calculi. We present various formal systems studied in the literature
and discuss their distinctive features, emphasizing on expressiveness, axiomatic systems, and (un)decidability results
On Propositional Interval Neighborhood Temporal Logics
Full text linkLogics for time intervals provide a natural framework for dealing with time in various areas of computer science and artificial intelligence, such as planning, natural language processing, temporal databases, and formal specification. In this paper we focus our attention on propositional interval temporal logics with temporal modalities for neighboring intervals over linear orders. We study the class of propositional neigh-borhood logics (PNL) over two natural semantics, respectively admitting and excluding point-intervals. First, we introduce interval neighborhood frames and we provide representation theorems for them, then, we develop complete axiomatic systems and semantic tableaux for logics in PNL
Two-sorted point-interval temporal logics
No full textThere are two natural and well-studied approaches to temporal ontology and reasoning: point-based and interval-based. Usually, interval-based temporal reasoning deals with points as particular, duration-less intervals. Here we develop explicitly two-sorted point-interval temporal logical framework whereby time instants (points) and time periods (intervals) are considered on a par, and the perspective can shift between them within the formal discourse. We focus on fragments involving only modal operators that correspond to the inter-sort relations between points and intervals. We analyze their expressiveness, comparative to interval-based logics, and the complexity of their satisfiability problems. In particular, we identify some previously not studied and potentially interesting interval logics. © 2011 Elsevier B.V
From linear to branching-time temporal logics: transfer of semantics and definability
Full text linkThis paper investigates logical aspects of combining linear orders as semantics for modal and temporal logics, with modalities for possible paths, resulting in a variety of branching time logics over classes of trees. Here we adopt a unified approach to the Priorean, Peircean and Ockhamist semantics for branching time logics, by considering them all as fragments of the latter, obtained as combinations, in various degrees, of languages and semantics for linear time with a modality for possible paths. We then consider a hierarchy of natural classes of trees and bundled trees arising from a given class of linear orders and show that in general they provide different semantics. We also discuss transfer of definability from linear orders to trees and introduce a uniform translation from Priorean to Peircean formulae which transfers definability of properties of linear orders to definability of properties of all paths in trees
Propositional interval neighborhood logics: Expressiveness, decidability, and undecidable extensions
Full text linkIn this paper, we investigate the expressiveness of the variety of propositional interval neighborhood logics (PNL), we establish their decidability on linearly ordered domains and some important subclasses, and we prove the undecidability of a number of extensions of PNL with additional modalities over interval relations. All together, we show that PNL form a quite expressive and nearly maximal decidable fragment of Halpern–Shoham’s interval logic HS
A General Tableau Method for Propositional Interval Temporal Logics
No full textLogics for time intervals provide a natural framework for
representing and reasoning about timing properties in various areas of
computer science. However, while various tableau methods have been de-
veloped for linear and branching time point-based temporal logics, not
much work has been done on tableau methods for interval-based temporal
logics. In this paper, we introduce a new, very expressive propositional
interval temporal logic, called (Non-Strict) Branching CDT (BCDT+)
which extends most of the propositional interval temporal logics pro-
posed in the literature. Then, we provide BCDT+ with a generic tableau
method which combines features of explicit tableau methods for modal
logics with constraint label management and the classical tableau method
for ̄rst-order logic, and we prove its soundness and completeness
Combining Linear Orders with Modalities for Possible Histories
No full textTwo main areas of temporal logics are those of linear time and of branching time. Linear orders, though, play a crucial role also in logics for branching time. Prior’s Ockhamist and Peircean semantical rules for branching time, in fact, involve quantification over histories in tree-like structures, where histories are maximal linearly ordered sets of moments. Moreover, this quantification can be viewed as the result of the application of a modal operator. This means that the language and semantics for branching time can be obtained as the combination of languages and semantics for linear time with a modality for possible histories. In this paper, we study various degrees of combining linear time and modal operators and semantics, and we discuss the problem of transferring logical properties from linear to branching time
Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers
No full textFront Matter, Table of Contents, Preface, Conference Organization, External Reviewer
Complete and Terminating Tableau for the Logic of Proper Subinterval Structures over Dense Orderings
Full text linkWe introduce special pseudo-models for the interval logic of proper subintervals over dense linear orderings. We prove finite model property with respect to such pseudo-models, and using that result we develop a decision procedure based on a sound, complete, and terminating tableau for that logic. The case of proper subintervals is essentially more complicated than the case of strict subintervals, for which we developed a similar tableau-based decision procedure in a recent work
- …
