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

Four Approaches to Automated Reasoning
with Differential Algebraic Structures

Jesus Aransay 1 , Clemens Ballarin 2 , and Julio Rubio 1

1 Dpto. de Matematicas y Computacion. Univ. de La Rioja. 26004 Logrono, Spain
{ jesus-maria.aransay,julio.rubio } @dmc.unirioja.es
2 Institut fur Informatik, Technische Univ. Munchen, D-85748 Garching, Germany
[e-mail]

Abstract. While implementing a proof for the Basic Perturbation

Lemma (a central result in Homological Algebra) in the theorem prover
Isabelle one faces problems such as the implementation of algebraic struc-
tures, partial functions in a logic of total functions, or the level of ab-
straction in formal proofs. Different approaches aiming at solving these
problems will be evaluated and classified according to features such as
the degree of mechanization obtained or the direct correspondence to
the mathematical proofs. From this study, an environment for further
developments in Homological Algebra will be proposed.

1 Introduction

EAT [15] and Kenzo [5] are software systems written under Sergeraert's direction
for symbolic computation in algebraic topology and homological algebra. These
systems have been used to compute remarkable results (for instance, some ho-
mology groups of iterated loop spaces) previously unknown. Both of them are
based on the intensive use of functional programming techniques, which enable
in particular to encode and handle at runtime the infinite data structures appear-
ing in algebraic topology algorithms. As pointed out in [4], algebraic topology
is a field where challenging problems remain open for computer algebra systems
and theorem provers.
In order to increase the reliability of the systems, a project to formally analyze
fragments of the programs was undertaken. In the last years, several results have
been found related to the algebraic specification of data structures, some of them
presented in [9]. Following these results, the algorithms dealing with these data
structures have to be studied. The long term goal of our research project is to
get certified versions of these algorithms, which would ensure the correctness
of the computer algebra systems to a degree much greater than current hand-
coded programs. To this end, a tool for extracting code from mechanized proofs
could be used. As a first step towards this general goal, our concrete objective
in this paper is to explore several possibilities to implement proofs of theorems
in algebraic topology by using a theorem prover. As theorem prover, the tactical

Partially supported by MCyT, project TIC2002-01626 and by CAR ACPI-2002/06.