© 1999 by Oxford University Press
| ||||||||||||||||||||||||||||||||||||||||||||||||||||
Undecidability of compass logic
A1 University of Amsterdam, Department of WINS, Plantage Muidergracht 24, 1018 TV Amsterdam, The Netherlands E-mail: marx@wins.uva.nl A2 School of Information Technology, Murdoch University, South Street, Murdoch 6150, Western Australia, Australia E-mail: m.reynolds@murdoch.edu.au
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