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

Revue:
Lecture Notes in Computer Science

ISSN: 0302-9743

Année de publication: 2007

Volumen: 4573 LNAI

Pages: 1-12

Type: Article

beta Ver similares en nube de resultados
SCOPUS: 2-s2.0-38049078571 WoS: WOS:000247859800001 GOOGLE SCHOLAR

D'autres publications dans: Lecture Notes in Computer Science

Projets liés

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

2006/00092/001

Résumé

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.