Download Combining Machine Learning and Theorem Proving in

e(=,e(*,2,1),1))),e(->,e(=,e(*,2,1),1),e(;,e(=,
e(*,1,1),2),e(=,e(*,2,1),2)))),e(&,e(->,e(=,e(*,1,2),2),
e(;,e(=,e(*,1,2),1),e(=,e(*,2,2),1))),e(->,
e(=,e(*,2,2),2),e(;,e(=,e(*,1,2),2),e(=,e(*,2,2),2)))))
Note the inclusion of a number of e(&, , ) expressions representing a conjunction
of various specific cases.
4.5
Identification of Solver Variables
The next stage of the process is a search through the expression to identify
any sub-expressions which represent variables in the solver formulation and
to replace them with those variables. This is performed recursively using the
replace constraint variable/2 predicate. For example, in finite algebras modelled
as multiplication tables, the solver formulation variables are the results of the *
operator on pairs of variables. Therefore, we can replace any occurrences of the
expression e(*,n,m) by the variable representing the result of n ∗ m (or the nth
row and mth column variable). It isn’t possible to replace all such expressions
with variables from the formulation, for instance the result of (1*1)*(2*2) is
the combination of two sub-results and cannot be simplified as a single solution
variable. In our example axiom, when we have searched and replaced solver
variables, our expression looks like this:
e(&,e(&,e(->,e(=,cvar(E 1 1),1),e(;,e(=,cvar(E 1 1),1)
,e(=,cvar(E 2 1),1))),e(->,e(=,cvar(E 2 1),1),e(;,
e(=,cvar(E 1 1),2),e(=,cvar(E 2 1),2)))),e(&,e(->,
e(=,cvar(E 1 2),2),e(;,e(=,cvar(E 1 2),1),e(=,
cvar(E 2 2),1))),e(->,e(=,cvar(E 2 2),2),e(;,
e(=,cvar(E 1 2),2),e(=,cvar(E 2 2),2)))))
where, for example, the expression e(*,1,1) has been replaced by the solver
variable E 1 1 and enclosed with cvar(. . . ) for easy identification later.
4.6
Converting to Constraints
The last stage of the translation process deals with converting the expanded expressions, in the form of e(operator,sub1,sub2) into constraints on the variables
of the CSP solver formulation. This part of the process is somewhat system
specific in that the constraints must obey the syntax of the underlying CSP
solving system, in our case Sicstus Prolog. The most straightforward method
of converting expressions to constraint statements is to write write to standard output, redirecting as necessary for output to persistent storage. This is
achieved using the convert/1 predicate.
30