Listar Artículos (Ciencias de la Computación e Inteligencia Artificial) por autor 

Listar Artículos (Ciencias de la Computación e Inteligencia Artificial) por autor "Ruiz Reina, José Luis"                

Mostrando ítems 1-12 de 12

    • Ponencia
      Icon

      A Formal Proof of Dickson’s Lemma in ACL2 

      Martín Mateos, Francisco Jesús; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Ruiz Reina, José Luis (Springer, 2003)
      Dickson’s Lemma is the main result needed to prove the termination of Buchberger’s algorithm for computing Gr¨obner basis ...
    • 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

      Constructing Formally Verified Reasoners for the ALC Description Logic 

      Hidalgo Doblado, María José; Alonso Jiménez, José Antonio; Martín Mateos, Francisco Jesús; Ruiz Reina, José Luis (Elsevier, 2008)
      Description Logics are a family of logics used to represent and reason about conceptual and terminological knowledge. ...
    • Artículo
      Icon

      Efficient execution in an automated reasoning environment 

      Greve, David A.; Kaufmann, Matt; Manolios, Panagiotis; Moore, J. Strother; Ray, Sandip; Ruiz Reina, José Luis; Sumners, Rob; Vroon, Daron; Wilding, Matthew (Cambridge University Press, 2008)
      We describe a method that permits the user of a mechanized mathematical logic to write elegant logical definitions while ...
    • Artículo
      Icon

      Formal Correctness of a Quadratic Unification Algorithm 

      Ruiz Reina, José Luis; Martín Mateos, Francisco Jesús; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José (Springer, 2006)
      We present a case study using ACL2 [5] to verify a non-trivial algorithm that uses efficient data structures. The algorithm ...
    • 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

      Formal verification of a generic framework to synthesize SAT-provers 

      Martín Mateos, Francisco Jesús; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Ruiz Reina, José Luis (Springer, 2004)
      We present in this paper an application of the ACL2 system to generate and reason about propositional satis ability ...
    • 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

      Formally Verified Tableau-Based Reasoners for a Description Logic 

      Hidalgo Doblado, María José; Alonso Jiménez, José Antonio; Borrego Díaz, Joaquín; Martín Mateos, Francisco Jesús; Ruiz Reina, José Luis (Springer, 2014)
      Description Logics are a family of logics used to represent and reason about conceptual and terminological knowledge. One ...
    • 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. ...
    • Artículo
      Icon

      Verification of the Formal Concept Analysis 

      Alonso Jiménez, José Antonio; Borrego Díaz, Joaquín; Hidalgo Doblado, María José; Martín Mateos, Francisco Jesús; Ruiz Reina, José Luis (Real Academia de Ciencias, 2004)
      This paper is concerned with a formal verification of the Formal Concept Analysis framework. We use the PVS system to ...
    • Artículo
      Icon

      Verifying the bridge between simplicial topology and algebra: the Eilenberg–Zilber algorithm 

      Lambán Pardo, Laureano; Rubio, Julio; Martín Mateos, Francisco Jesús; Ruiz Reina, José Luis (Oxford Academic, 2013)
      The Eilenberg–Zilber algorithm is one of the central components of the computer algebra system called Kenzo, devoted ...