Buscar
Mostrando ítems 1-4 de 4
Artículo
Proof Pearl: a Formal Proof of Higman’s Lemma in ACL2
(Springer, 2011)
Higman’s lemma is an important result in infinitary combinatorics, which has been formalized in several theorem provers. In this paper we present a formalization and proof of Higman’s Lemma in the ACL2 theorem prover. ...
Artículo
Formalization of a normalization theorem in simplicial topology
(Springer, 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, ...
Artículo
Formal proofs about rewriting using ACL2
(Springer, 2002)
We present an application of the ACL2 theorem prover to reason about rewrite systems theory. We describe the formalization and representation aspects of our work using the firstorder, quantifier-free logic of ACL2 and ...
Artículo
A verified Common Lisp implementation of Buchberger's algorithm in ACL2
(Elsevier, 2010)
In this article, we present the formal verification of a Common Lisp implementation of Buchberger's algorithm for computing Gröbner bases of polynomial ideals. This work is carried out in ACL2, a system which provides ...