Executing in Common Lisp, Proving in ACL2.

  1. Andrés, M. 1
  2. Lambán, L. 1
  3. Rubio, J. 1
  1. 1 Universidad de La Rioja
    info

    Universidad de La Rioja

    Logroño, España

    ROR https://ror.org/0553yr311

Aldizkaria:
Lecture Notes in Computer Science

ISSN: 0302-9743

Argitalpen urtea: 2007

Alea: 4573 LNAI

Orrialdeak: 1-12

Mota: Artikulua

SCOPUS: 2-s2.0-38049078571 WoS: WOS:000247859800001 GOOGLE SCHOLAR

Beste argitalpen batzuk: Lecture Notes in Computer Science

Lotura duten proiektuak

Sistemas de cálculo simbólico: nuevos desarrollos en topología algebráica y fiabilidad

2006/00092/001

Laburpena

In this paper, an approach to integrate an already-written Common Lisp program for algebraic manipulation with ACL2 proofs of properties of that program is presented. We report on a particular property called "cancellation theorem", which has been proved in ACL2, and could be applied to several problems in the field of Computational Algebraic Topology. © Springer-Verlag Berlin Heidelberg 2007.