A logic of motion

There are numerous applications such as air traffic manage- ment, cellular phone location tracking, and vehicle protection systems where there is a critical need to reason about moving objects. In this paper, we propose a formal logic of motion (LOM for short). We provide a formal syntax for LOM, as well as a model theory for LOM. In addition, we develop al- gorithms to check consistency of LOM theories, as well as to answer certain kinds of queries posed to LOM theories. We have implemented these algorithms in a prototype LOM sys- tem - we describe experiments showing that such queries can be efficiently executed in practice.