Next: About this document
Formalisation of the Decision Procedure Model
In this page we translate the information in Figure 2.6
into a more conventional logical notation, ready for further
refinement. As in the translation of our operator diagram, the
algorithm looks complex but can be automated.
Our method for this is as follows:
- Construct the top-level expression:
- Look up the top-level procedure on the diagram, which is of the
form
. Construct an expression:
where
each
is a new variable restricted to type
.
For example the top-level expression in Figure 2.6 is:
.
- For each function oval, labelled F, on the diagram, find the
set, D, consisting of the data types
on which it
depends (found by following backwards along the arrows on the diagram to its
data sources) and the type
of its result. Now construct a term
where
each
is either a variable
, if
is the same type as
, or, if not, is a new variable. Any new variables are
existentially quantified. For example the
function on
Figure 2.6 yields the expression:
.
- Construct the expression:
, the left side of which comes from the first step and
where C is the conjunction of all the terms from the
previous step. For our example, this gives us
expression 1 shown below.
- For each function oval, labelled F, find the set of data types
on which it depends (by following backwards
along the arrows on the diagram to its data sources). Find the set of
data types
which the function produces (by
following the arrows leading out of its oval). Construct an
expression
where each
is a new variable restricted to type
.
All the variables
are existentially quantified.
For example the
function oval in Figure 2.6
yields expression 2 shown below.
We have a risk assessment for a person and some data source if there
is some model which we can select for that person and data, and we can
assess the loan risk based on that model.

For every person and data store we can select some model.

Next: About this document
Dave Stuart Robertson
Tue Jul 7 10:24:06 BST 1998