1,721,126 research outputs found
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
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
A General Tableau Method for Propositional Interval Temporal Logics: Theory and Implementation
No full textIn this paper, we focus our attention on tableau methods for propositional interval temporal logics. These logics provide a natural framework for representing and reasoning about temporal properties in several areas of computer science. However, while various tableau methods have been developed
for linear and branching time point-based temporal logics, not much work has been done on tableau methods for interval-based ones. We develop a general tableau method for Venema’s CDT logic interpreted over partial orders (BCDT+ for short). It combines features of the classical tableau method for first-order logic with those of explicit tableau methods for modal logics with constraint label management, and it can be easily tailored to most propositional interval temporal logics proposed in
the literature. We prove its soundness and completeness, and we show how it has been implemented
Interval Temporal Logics: a Journey
No full textWe discuss a family of modal logics for reasoning about relational structures
of intervals over (usually) linear orders, with modal operators associated
with the various binary relations between such intervals, known as
Allen’s interval relations. The formulae of these logics are evaluated at
intervals rather than points and the main effect of that semantic feature is
substantially higher expressiveness and computational complexity of the interval
logics as compared to point-based ones. Without purporting to provide
a comprehensive survey of the field, we take the reader to a journey
through the main developments in it over the past 10 years and outline some
landmark results on expressiveness and (un)decidability of the satisfiablity
problem for the family interval logic
Crossing the Undecidability Border with Extensions of Propositional Neighborhood Logic over Natural Numbers
No full textPropositional Neighborhood Logic (PNL) is an interval temporal logic featuring two modalities corresponding to the relations of right and left neighborhood between two intervals on a linear order (in terms of Allen's relations, meets and met by). Recently, it has been shown that PNL interpreted over several classes of linear orders, including natural numbers, is decidable (NEXPTIME-complete) and that some of its natural extensions preserve decidability. Most notably, this is the case with PNL over natural numbers extended with a limited form of metric constraints and with the future fragment of PNL extended with modal operators corresponding to Allen's relations begins, begun by, and before. This paper aims at demonstrating that PNL and its metric version MPNL, interpreted over natural numbers, are indeed very close to the border with undecidability, and even relatively weak extensions of them become undecidable. In particular, we show that (i) the addition of binders on integer variables ranging over interval lengths makes the resulting hybrid extension of MPNL undecidable, and (ii) a very weak first-order extension of the future fragment of PNL, obtained by replacing proposition letters by a restricted subclass of first-order formulae where only one variable is allowed, is undecidable (in contrast with the decidability of similar first-order extensions of point-based temporal logics)
A syntactic realization theorem for justification logics
No full textJustification logics are refinements of modal logics where modalities are replaced by justification terms. They are connected to modal logics via so-called realization theorems. We present a syntactic proof of a single realization theorem that uniformly connects all the normal modal logics formed from the axioms \$mathsfd\$, \$mathsft\$, \$mathsfb\$, \$mathsf4\$, and \$mathsf5\$ with their justification counterparts. The proof employs cut-free nested sequent systems together with Fitting's realization merging technique. We further strengthen the realization theorem for \$mathsfKB5\$ and \$mathsfS5\$ by showing that the positive introspection operator is superfluous
Expressiveness of the Interval Logics of Allen's Relations on the Class of all Linear Orders: Complete Classification
No full textWe compare the expressiveness of the fragments of Halpern and Shoham’s interval logic (HS), i.e., of all interval logics with modal operators associated with Allen’s relations between intervals in linear orders. We establish a complete set of interdefinability equations between these modal operators, and thus obtain a complete classification of the family of 212 fragments of HS with respect to their expressiveness. Using that result and a computer program, we have found that there are 1347 expressively different such interval logics over the class of all linear orders
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
Undecidability of the Logic of the Overlap Relation over Discrete Linear Orderings
No full textThe validity/satisfiability problem for most propositional interval temporal logics is (highly) undecidable,
under very weak assumptions on the class of interval structures in which they are interpreted. That, in
particular, holds for most fragments of Halpern and Shoham’s interval modal logic HS. Still, decidability
is the rule for the fragments of HS with only one modal operator, based on an Allen’s relation. In this
paper, we show that the logic O of the Overlap relation, when interpreted over discrete linear orderings, is
an exception. The proof is based on a reduction from the undecidable octant tiling problem. This is one of
the sharpest undecidability result for fragments of HS
- …
