Journal of Logic and Computation, Volume 9, Issue 6, pp. 897-914: Abstract.
Undecidability of compass logic
M Marx1 and M Reynolds2
1University of Amsterdam, Department of WINS, Plantage Muidergracht 24, 1018 TV Amsterdam, The Netherlands, E-mail: email@example.com, 2School of Information Technology, Murdoch University, South Street, Murdoch 6150, Western Australia, Australia, E-mail: firstname.lastname@example.org
It is known that the tiling technique can be used to give simple proofs of undecidability of various two-dimensional modal and temporal logics. However, up until now, the simplest two-dimensional temporal logic, the compass logic of Venema, has eluded such treatment. We present a new coding of an enumeration of the tiling plane which enables us to show that the compass logic is undecidable.
Keywords: Temporal logic, two-dimensional modal logic, decision problems, tiling