| Abstract | Yaman et. al. [Yaman et al., 2004] introduce “gotheories” to reason about moving objects. In this
paper, we show that this logic often does not allow
us to infer that an object is not present at a given
place or region, even though common sense would
dictate that this is a reasonable inference to make.
We define a class of models of go-theories called
coherent models. We use this concept to define a
motion closed world assumption (MCWA) and de-
velop a notion of MCWA-entailment. We show
that checking if a go-theory has a coherent model
is NP-complete. An in atom checks if a given ob-
ject is present in a given region sometime in a given
time interval. We provide sound and complete al-
gorithms to check if a ground in literal (positive
or negative in atom) can be inferred from a go-
theory using the MCWA. In our experiments our
algorithms answer such queries in less than 1 sec-
ond when there are up to 1,000 go-atoms per object.
|
