Interval logics formalize temporal reasoning on interval structures over linearly (or partially) ordered domains, where time intervals are the primitive ontological entities and truth of formulae is defined relative to time intervals, rather than time points. In this paper, we introduce and study Metric Propositional Neighborhood Logic (MPNL) over natural numbers. MPNL features two modalities referring, respectively, to an interval that is ``met by" the current one and to an interval that ``meets" the current one, plus an infinite set of length constraints, regarded as atomic propositions, to constrain the length of intervals. We argue that MPNL can be successfully used in different areas of computer science to combine qualitative and quantitative interval temporal reasoning, thus providing a viable alternative to well-established logical frameworks such as Duration Calculus. We show that MPNL is decidable in double exponential time and expressively complete with respect to a well-defined sub-fragment of the two-variable fragment FO2[N,=,<,s] of first-order logic for linear orders with successor function, interpreted over natural numbers. Moreover, we show that MPNL can be extended in a natural way to cover full FO2[N,=,<,s], but, unexpectedly, the latter (and hence the former) turns out to be undecidable.

Metric propositional neighborhood logics on natural numbers

DELLA MONICA, Dario;MONTANARI, Angelo;
2013-01-01

Abstract

Interval logics formalize temporal reasoning on interval structures over linearly (or partially) ordered domains, where time intervals are the primitive ontological entities and truth of formulae is defined relative to time intervals, rather than time points. In this paper, we introduce and study Metric Propositional Neighborhood Logic (MPNL) over natural numbers. MPNL features two modalities referring, respectively, to an interval that is ``met by" the current one and to an interval that ``meets" the current one, plus an infinite set of length constraints, regarded as atomic propositions, to constrain the length of intervals. We argue that MPNL can be successfully used in different areas of computer science to combine qualitative and quantitative interval temporal reasoning, thus providing a viable alternative to well-established logical frameworks such as Duration Calculus. We show that MPNL is decidable in double exponential time and expressively complete with respect to a well-defined sub-fragment of the two-variable fragment FO2[N,=,<,s] of first-order logic for linear orders with successor function, interpreted over natural numbers. Moreover, we show that MPNL can be extended in a natural way to cover full FO2[N,=,<,s], but, unexpectedly, the latter (and hence the former) turns out to be undecidable.
File in questo prodotto:
File Dimensione Formato  
10.1007_s10270-011-0195-y.pdf

non disponibili

Tipologia: Documento in Post-print
Licenza: Non pubblico
Dimensione 992.56 kB
Formato Adobe PDF
992.56 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11390/871910
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 20
  • ???jsp.display-item.citation.isi??? 13
social impact