Decision procedures must be interfaced with the data structures used in any program. This is done by specifying how each primitive should be evaluated in terms of data structures and program functions. In the case of properties and relations one needs to specify how given the appropriate arguments a Boolean value should be returned.
For example, the topological connectedness relation might be defined as follows:
where get_region(x) returns some data structure representing the region associated with object x and regions_connect(x,y) computes whether the structures x and y correspond to regions which are connected.
If the theory contains functional expressions these will also need to be defined. (An example of a function useful in specifying spatial relationships is the `convex-hull' of a region, which is the smallest convex region in which it is contained.)
Programmers must take great care that the primitive definitions accurately correspond to the concepts of the DP. This is necessary if all inferences drawn by the DP are to be valid with respect to the program data. If the definition is not correct then the DP may not be able to compute all inferences which can be validly drawn from the data. More seriously, the DP may draw inferences which are not true. The primitives concepts of each DP are described by a (fairly small) set of axioms. The programmer must ensure that definitions of primitives obey all these axioms. He must also realise that properties of data which are not captured by these axioms are not known to the decision procedure.
The ability to interface DPs with arbitrary data-models allows the programmer complete freedom in the low-level details of data storage and manipulation. However once the primitives of a DP have been defined the programmer can employ a flexible language of high-level concepts without having to think about the data.