Now showing items 1-5 of 5
Formalization of a normalization theorem in simplicial topology [Article]
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, ...
A verified Common Lisp implementation of Buchberger's algorithm in ACL2 [Article]
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 ...
Modelling algebraic structures and morphisms in ACL2 [Article]
In this paper, we present how algebraic structures and morphisms can be modelled in the ACL2 theorem prover. Namely, we provide a guide- line to implement a set of tools that facilitates the formalisations related ...
Formal proofs about rewriting using ACL2 [Article]
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 ...
Proof Pearl: a Formal Proof of Higman’s Lemma in ACL2 [Article]
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. ...