Executing in Common Lisp, Proving in ACL2.
- Andrés, M. 1
- Lambán, L. 1
- Rubio, J. 1
-
1
Universidad de La Rioja
info
ISSN: 0302-9743
Year of publication: 2007
Volume: 4573 LNAI
Pages: 1-12
Type: Article
More publications in: Lecture Notes in Computer Science
Related Projects
Abstract
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.