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

Revista:
Lecture Notes in Computer Science

ISSN: 0302-9743

Ano de publicación: 2007

Volume: 4573 LNAI

Páxinas: 1-12

Tipo: Artigo

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

Outras publicacións en: Lecture Notes in Computer Science

Proxectos relacionados

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

2006/00092/001

Resumo

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.