Conference paper
Right Propositional Neighborhood Logic over Natural Numbers with Integer Constraints for Interval Lengths
Interval temporal logics are based on interval structures over linearly (or partially) ordered domains, where time intervals, rather than time instants, are the primitive ontological entities. In this paper we introduce and study Right Propositional Neighborhood Logic over natural numbers with integer constraints for interval lengths, which is a propositional interval temporal logic featuring a modality for the 'right neighborhood' relation between intervals and explicit integer constraints for interval lengths.
We prove that it has the bounded model property with respect to ultimately periodic models and is therefore decidable. In addition, we provide an EXP SPACE procedure for satisfiability checking and we prove EXPSPACE-hardness by a reduction from the exponential corridor tiling problem.
| Language: | English |
|---|---|
| Publisher: | IEEE Computer Society Press |
| Year: | 2009 |
| Pages: | 240-249 |
| Proceedings: | Seventh IEEE International Conference on Software Engineering and Formal Methods |
| ISBN: | 0769538703 , 1509068759 , 9780769538709 and 9781509068753 |
| Types: | Conference paper |
| DOI: | 10.1109/SEFM.2009.36 |
Artificial intelligence Calculus Computer science Constraint theory Databases EXPSPACE hardness Logic Natural language processing Ontologies Real time systems Software engineering computability exponential corridor tiling problem integer constraint interval length interval structure interval temporal logic primitive ontological entity propositional interval temporal logic right propositional neighborhood logic satisfiability checking temporal logic time interval
