Pub-miscellaneous-applications
Miscellaneous Applications
- Verifying the
bridge between simplicial topology and algebra: the Eilenberg-Zilber
algorithm, L. Lamban, J. Rubio, F. J. Martin-Mateos and
J. L. Ruiz-Reina. Logic Journal of the IGPL 22(1),
pp. 39-65, 2014. The Eilenberg-Zilber algorithm is one of the central
components of the computer algebra system called Kenzo, devoted
to computing in Algebraic Topology. In this article we report on a
complete formal proof of the underlying
Eilenberg-Zilber theorem, using the ACL2 theorem prover. As our
formalization is executable, we are able to compare the results of the
certified programme with those of Kenzo on
some universal examples. Since the results coincide, the
reliability of Kenzo is reinforced. This is a new step in our
long-term project towards certified programming for Algebraic
Topology.
- [Note: This entry extends an earlier version, included just below.]
Formalization of a normalization theorem in simplicial
topology, L. Lamban, F. J. Martin-Mateos,
J. Rubio and J. L. Ruiz-Reina. Annals of Mathematics and
Artificial Intelligence 64(1), pp. 1-37, 2012. In this paper
we present a complete formalization of the Normalization Theorem,
a result in Algebraic Simplicial Topology stating that there
exists a homotopy equivalence between the chain complex of a
simplicial set, and a smaller chain complex for the same
simplicial set, called the normalized chain complex. Even if the
Normalization Theorem is usually stated as a higher-order result
(with a Category Theory flavor) we manage to give a first-order
proof of it. To this aim it is instrumental the introduction of an
algebraic data structure called simplicial polynomial. As a
demonstration of the validity of our techniques we developed a
formal proof in the ACL2 theorem prover.
- [Note: See entry just above for an extended version.]
Applying ACL2 to the Formalization of Algebraic Topology: Simplicial
Polynomials, L. Lamban, F. J. Martin-Mateos, J. Rubio
and J. L. Ruiz-Reina. ITP 2011 - LNCS 6898, pp. 200-215, 2011.
In this paper we present a complete formalization of the Normalization
Theorem, a result in Algebraic Simplicial Topology stating that there
exists a homotopy equivalence between the chain complex of a simplicial
set, and a smaller chain complex for the same simplicial set, called the
normalized chain complex.
-
ACL2 verification of simplicial degeneracy programs in the Kenzo
system,
F.J. Martin-Mateos, J. Rubio and J.L. Ruiz-Reina.
Calculemus 2009 - LNAI 5625, pp. 106-121, 2009.
In this paper, we give a complete automated proof of the correctness of
the encoding of degeneracy lists (a topological object) used in Kenzo,
a Computer Algebra System devoted to Algebraic Topology.
- A verified
Common Lisp implementation of Buchberger's algorithm in ACL2.
I. Medina Bulo, F. Palomo Lozano, and J. L. Ruiz Reina. Journal of
Symbolic Computation 45-1:96-123. 2010. In this article, we
present the formal verification of a Common Lisp implementation of
Buchberger's algorithm for computing Groebner bases of polynomial
ideals. This work is carried out in ACL2, a system which provides an
integrated environment where programming (in a pure functional subset
of Common Lisp) and formal verification of programs, with the
assistance of a theorem prover, are possible. Our implementation is
written in a real programming language and it is directly executable
within the ACL2 system or any compliant Common Lisp system. We provide
here snippets of real verified code, discuss the formalization details
in depth, and present quantitative data about the proof effort.
-
Formal Verification of Molecular Computational Models in ACL2:
A Case Study,
F.J. Martin-Mateos, J.A. Alonso, M.J. Hidalgo and J.L. Ruiz-Reina.
CAEPIA 2003 - LNCS 3040, pp. 344-353, 2004.
A formalization in ACL2 of Lipton's experiment that uses DNA computation
for solving SAT.
-
Verified Computer Algebra in ACL2 (Groebner Bases Computation), I.
Medina Bulo, F. Palomo Lozano, J. A. Alonso Jimenez and J. L. Ruiz
Reina, Artificial Intelligence and Symbolic Mathematical Computation
(AISC 2004) , LNAI 3249:171-184. Linz (Austria), 2004. In this paper, we
present the formal verification of a Common LISP implementation of
Buchberger's algorithm for computing Groebner bases of polynomial ideals.
This work is carried out in the ACL2 system and shows how verified Computer
Algebra can be achieved in an executable logic.
-
Verification of an In-place Quicksort in ACL2, Sandip Ray and Rob Sumners.
In D. Borrione, M. Kaufmann,
and J S. Moore, editors, Proceedings of the 3rd
International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2
2002), Grenoble, France, April 2002, pages 204-212.
- A Mechanical Proof of the
Chinese Remainder Theorem, David Russinoff, in Proceedings of
ACL2 Workshop 2000.
- Knuth's Generalization of McCarthy's 91 Function, John Cowles, Chapter 17
of Computer-Aided Reasoning: ACL2 Case
Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000.
(ACL2 scripts are available from
directory 1999/knuth-91/ in the community-books.)
This article deals with a challenge by Donald Knuth for a “proof
by computer” of a theorem about his generalization of John McCarthy's famous
“91 function.” The generalization involves real numbers, and the case
study uses ACL2 to meet Knuth's challenge by mechanically verifying results
not only about the field of all real numbers, but also about every subfield
of that field. The ACL2 scripts referenced here provide the full details of
the results described in the article along with solutions to all the
exercises in the article.
-
Verification of Year 2000 Conversion Rules, Matt Kaufmann, March 1999
(revised from June 1999). This page links to event files in support
of the paper Verification of Year 2000 Conversion Rules Using the
ACL2 Theorem Prover', in Software Tools for
Technology Transfer. This formal verification of COBOL
transformation rules was done in support of Y2K remediation performed
at EDS CIO Services using an in-house proprietary tool, Cogen 2000.
- A Mechanically Checked Proof of a Comparator Sort Algorithm,
J Moore and B. Brock,
in, M. Broy, J. Gruenbauer, D. Harel, and
C. A. R. Hoare (eds.)
Engineering Theories of Software Intensive Systems,
Springer NATO Science Series II, 195, pp. 141-175, 2005.
This paper describes a mechanically checked correctness proof for the
comparator sort algorithm underlying a microcode program in a commercially
designed digital signal processing chip. The abstract algorithm uses an
unlimited number of systolic comparator modules to sort a stream of data. In
addition to proving that the algorithm produces an ordered permutation of its
input, two theorems are proved that are important to verifying the microcode
implementation. These theorems describe how positive and negative
“infinities” can be streamed into the array of comparators to achieve
certain effects. Interesting generalizations are necessary in order to prove
these theorems inductively.
(ACL2 Script)
- The
Specification of a Simple Autopilot in ACL2, Bill Young, July, 1996.
This paper presents an ACL2 translation of Butler's PVS formalization of a
simple autopilot.
