Four approaches to automated reasoning with differential algebraic structures
- Aransay, J. 1
- Ballarin, C. 2
- Rubio, J. 1
-
1
Universidad de La Rioja
info
-
2
Technical University Munich
info
ISSN: 0302-9743
Argitalpen urtea: 2004
Alea: 3249
Orrialdeak: 222-235
Mota: Artikulua
beta Ver similares en nube de resultadosBeste argitalpen batzuk: Lecture Notes in Computer Science
Laburpena
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 structures, partial functions in a logic of total functions, or the level of abstraction 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. © Springer-Verlag 2004.