Listar Ciencias de la Computación e Inteligencia Artificial por materia 

ListarCiencias de la Computación e Inteligencia Artificial por materia "ACL2"

Mostrando ítems 1-6 de 6

    • Artículo
      Icon

      A verified Common Lisp implementation of Buchberger's algorithm in ACL2 

      Medina Bulo, Inmaculada; Palomo Lozano, Francisco; Ruiz Reina, José Luis (Elsevier, 2010)
      In this article, we present the formal verification of a Common Lisp implementation of Buchberger's algorithm for ...
    • Artículo
      Icon

      Formal proofs about rewriting using ACL2 

      Ruiz Reina, José Luis; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Martín Mateos, Francisco Jesús (Springer, 2002)
      We present an application of the ACL2 theorem prover to reason about rewrite systems theory. We describe the formalization ...
    • Artículo
      Icon

      Formalization of a normalization theorem in simplicial topology 

      Lambán Pardo, Laureano; Martín Mateos, Francisco Jesús; Rubio, Julio; Ruiz Reina, José Luis (Springer, 2012)
      In this paper we present a complete formalization of the Normalization Theorem, a result in Algebraic Simplicial Topology ...
    • Artículo
      Icon

      Modelling algebraic structures and morphisms in ACL2 

      Heras, Jónathan; Martín Mateos, Francisco Jesús; Pascual, Vico (Springer, 2015)
      In this paper, we present how algebraic structures and morphisms can be modelled in the ACL2 theorem prover. Namely, we ...
    • Artículo
      Icon

      Proof Pearl: a Formal Proof of Higman’s Lemma in ACL2 

      Martín Mateos, Francisco Jesús; Ruiz Reina, José Luis; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José (Springer, 2011)
      Higman’s lemma is an important result in infinitary combinatorics, which has been formalized in several theorem provers. ...
    • Ponencia
      Icon

      Using Abstract Stobjs in ACL2 to Compute Matrix Normal Forms 

      Lambán Pardo, Laureano; Martín Mateos, Francisco Jesús; Rubio, Julio; Ruiz Reina, José Luis (Springer, 2017)
      We present here an application of abstract single threaded objects (abstract stobjs) in the ACL2 theorem prover, to define ...