Reasoning about motion: product theories of motion

This paper describes a technique of combining two theories to obtain a combined theory called the product theory. We combine theories of time and space to obtain a product theory useful in modeling motion and motion planning. We begin by combining propositional temporal logic (PTL) with itself to obtain a two dimensional temporal logic (2D-TL). 2D-TL is expressive enough to represent useful motion information. Though PTL itself is decidable, we are able to express any instance of the post correspondence problem as a formula of 2D-TL. This proves 2D-TL to be undecidable.<>