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

Zeitschrift:
Lecture Notes in Computer Science

ISSN: 0302-9743

Datum der Publikation: 2007

Ausgabe: 4573 LNAI

Seiten: 1-12

Art: Artikel

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

Andere Publikationen in: Lecture Notes in Computer Science

Projekte im Zusammenhang

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

2006/00092/001

Zusammenfassung

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.