Four approaches to automated reasoning with differential algebraic structures

  1. Aransay, J. 1
  2. Ballarin, C. 2
  3. Rubio, J. 1
  1. 1 Universidad de La Rioja
    info

    Universidad de La Rioja

    Logroño, España

    ROR https://ror.org/0553yr311

  2. 2 Technical University Munich
    info

    Technical University Munich

    Múnich, Alemania

    ROR https://ror.org/02kkvpp62

Revista:
Lecture Notes in Computer Science

ISSN: 0302-9743

Año de publicación: 2004

Volumen: 3249

Páginas: 222-235

Tipo: Artículo

SCOPUS: 2-s2.0-33646015242 WoS: WOS:000224110900019 GOOGLE SCHOLAR

Otras publicaciones en: Lecture Notes in Computer Science

Resumen

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.