Extending Topological Nexttime Logic
Subsequently, we give two extensions of topological nexttime logic, TNL; see . The first of the corresponding formal systems enables one to reason about the change of sets in the course of (discrete) time. The second incorporates the notion of complementation into TNL. We establish corresponding completeness, decidability and - concerning the first system - complexity results. As to the latter we obtain a 'low' complexity of the satisfiability problem since the time operators involved are comparatively weak: NP-completeness. Applications of the systems to various fields of spatio-temporal reasoning are intended.
Nutzung und Vervielfältigung:
Alle Rechte vorbehalten