Four Approaches to Automated Reasoning with Differential Algebraic Structures - Artificial Intelligence and Symbolic Computation - page 226

computer system employed into the elementsofmathematics.Thisprocessisof
great importance, since it may clarify what has been done and to which extent
we can rely on the results obtained in the computer, and will be briefly described
at the end of this section; for this symbolic approach, the abstraction process
can lead to identify the different structures embedding homomorphisms with a
simple structure embedding all of them; the idea will be again used in Section 5
and its importance will be observed also in Section 6.
The proof of Lemma 2 illustrates most of the problems that have to be solved:
the implementation of complex algebraic structures and the implementation of
homomorphisms. In addition, one must work with the homomorphisms in two
different levels simultaneously: equationally, like elements of an algebraic struc-
ture, and also like functions over a concrete domain and codomain. These reasons
made us choose this lemma to seek the more appropriate framework. Along this
section this framework is precisely defined in the symbolic approach, then the
proved lemmas are explained and finally some properties of this framework are
enumerated 1 .
The following abstractions can be carried out:

- The big chain complex ( D ,d D ∗ ) is by definition a graded group with a

differential operator, and (ker p, d D ∗ ) is a chain subcomplex of it. The endo-
morphisms of ( D

∗

,d D ∗ ) are the elements of a generic ring R .
- Some special homomorphisms between ( D

∗

)anden-
domorphisms of (ker p, d D ∗ ) are seen as elements of R (for instance, the
identity, the null homomorphism or some contractions).

,d D ∗ )and(ker p, d D ∗

∗

Some of the computations developed under this construction of a generic ring
can be then identified with some parts of the proof of Lemma 2. On the other
hand, some other properties can not be proved in this framework since some
(relevant) information about the structures involved and their properties is lost.
This framework, being too generic, permits to avoid the problems of the concrete
implementation of homomorphisms.
We will now give an example of how some of the properties having to be
proved in the lemma can be represented in this framework. According to Def. 2
we have to prove the 5 characteristic properties of the reduction given in the
conclusion of the lemma. From the five equalities, two fit in this framework and
can be derived equationally inside of it. The first one is property (5), i.e.

hh =0 R

The proof is trivial since the statement follows directly from premises of
Lemma 2 and its proof can be implemented as in the mathematical proof. The
second example of a proof that can be given inside this framework is property
(3), i.e.

if hdh = h and hh =0and p = dh + hd then (1 R − p ) h =0 R ,

whose implementation in Isabelle can be given as

1 A similar pattern will be followed in the other approaches.