The function of a logical decision procedure is to decide whether some
fact (represented in some logical notation) is a consequence of a set
of facts (represented in the same notation). All logical languages are
equipped with a set of inference rules which allow one to draw
conclusions from sets of formulae. However, demonstrating that a
consequence follows from some set of formulae may require a long
series of successive applications of inference rules --- this is
called a proof. For most sufficiently expressive logical
languages there is no general method of deciding (in finite time)
whether such a proof exists.
This
undecidability is one of the main reasons why logic is not more
widely used in computer science.
Logical languages normally enable one to reason about arbitrary `non-logical' properties and relations. However, by restricting their vocabulary to specific concepts obeying fixed axioms --- i.e.\ governed by a theory --- it is in many cases possible to devise algorithms which will decide in finite time whether a consequence holds. Such decision procedures are known for several theories of spatial and temporal concepts. It is the specification of such theories and construction of decision procedures which will form the major part of the theoretical aspect of our project.