Browsing Ciencias de la Computación e Inteligencia Artificial by Subject "ACL2"
Now showing items 1-6 of 6
-
Article
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 ...
-
Article
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 ...
-
Article
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 ...
-
Article
Modelling algebraic structures and morphisms in ACL2
(Springer, 2015)In this paper, we present how algebraic structures and morphisms can be modelled in the ACL2 theorem prover. Namely, we ...
-
Article
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. ...
-
Presentation
Using Abstract Stobjs in ACL2 to Compute Matrix Normal Forms
(Springer, 2017)We present here an application of abstract single threaded objects (abstract stobjs) in the ACL2 theorem prover, to define ...