- idUS
- Listar por autor
Listar por autor "Ruiz Reina, José Luis"
Mostrando ítems 1-20 de 32
-
Ponencia
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 ...
-
Ponencia
A Formally Verified Prover for the ALC Description Logic
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 (Springer, 2007)The Ontology Web Language (OWL) is a language used for the Semantic Web. OWL is based on Description Logics (DLs), a ...
-
Ponencia
A Generic Instantiation Tool and a Case Study: A Generic Multiset Theory.
Martín Mateos, Francisco Jesús; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Ruiz Reina, José Luis (University of Texas, 2002)In some cases, when we develop a formal theory in ACL2, it would be desirable that the definitions and theorems of the ...
-
Ponencia
A Theory About First-Order Terms in ACL2
Ruiz Reina, José Luis; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Martín Mateos, Francisco Jesús (University of Texas, 2002)We describe the development in ACL2 of a library of results about first-order terms. In particular, we present the ...
-
Artículo
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 ...
-
Ponencia
ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System
Martín Mateos, Francisco Jesús; Rubio, Julio; Ruiz Reina, José Luis (Springer, 2009)Kenzo is a Computer Algebra system devoted to Algebraic Topology, and written in the Common Lisp programming language. ...
-
Ponencia
Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials
Lambán Pardo, Laureano; Martín Mateos, Francisco Jesús; Rubio, Julio; Ruiz Reina, José Luis (Springer, 2011)In this paper we present a complete formalization, using the ACL2 theorem prover, of the Normalization Theorem, a result ...
-
Ponencia
Certified Symbolic Manipulation: Bivariate Simplicial Polynomials
Lambán Pardo, Laureano; Martín Mateos, Francisco Jesús; Rubio, Julio; Ruiz Reina, José Luis (ACM, 2013)Certified symbolic manipulation is an emerging new field where programs are accompanied by certificates that, suitably ...
-
Artículo
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. ...
-
Libro
Curso Práctico de Teoría de Conjuntos
Alonso Jiménez, José Antonio; Borrego Díaz, Joaquín; Pérez Jiménez, Mario de Jesús; Ruiz Reina, José Luis (Ediciones La Ñ, 1998)Todos los que hemos impartido tópicos diversos relativos a la Teoría de Conjuntos, en primer o segundo ciclo universitario, ...
-
Artículo
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
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
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 ...
-
Ponencia
Formal Reasoning about Efficient Data Structures: A Case Study in ACL2
Ruiz Reina, José Luis; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Martín Mateos, Francisco Jesús (Springer, 2003)We describe in this paper the formal verification, using the ACL2 system, of a syntactic unification algorithm where terms ...
-
Artículo
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 ...
-
Ponencia
Formal Verification of Molecular Computational Models in ACL2: A Case Study
Martín Mateos, Francisco Jesús; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Ruiz Reina, José Luis (Springer, 2003)Theorem proving is a classical AI problem with a broad range of applications. Since its complexity is exponential in the ...
-
Artículo
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 ...
-
Ponencia
Formalizing Rewriting in the ACL2 Theorem Prover
Ruiz Reina, José Luis; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Martín Mateos, Francisco Jesús (Springer, 2000)We present an application of the ACL2 theorem prover to formalize and reason about rewrite systems theory. This can be ...
-
Artículo
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 ...
-
Ponencia
Multiset Relations: A Tool for Proving Termination
Ruiz Reina, José Luis; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Martín Mateos, Francisco Jesús (University of Texas, 2000)