Author profile: Ruiz Reina, José Luis
Institutional data
Name | Ruiz Reina, José Luis |
Department | Ciencias de la Computación e Inteligencia Artificial |
Knowledge area | Ciencia de la Computación e Inteligencia Artificial |
Professional category | Profesor Titular de Universidad |
Request | |
Statistics
-
No. publications
32
-
No. visits
2891
-
No. downloads
5373
Publications |
---|
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 ... |
Presentation
Towards a verifiable topology of data
(Universidad de La Rioja, Departamento de Matemáticas y Computación, 2016)
|
Article
Formally Verified Tableau-Based Reasoners for a Description Logic
(Springer, 2014)
Description Logics are a family of logics used to represent and reason about conceptual and terminological knowledge. One ... |
Presentation
Proving and Computing: Applying Automated Reasoning to the Verification of Symbolic Computation Systems
(Springer, 2014)
The application of automated reasoning to the formal verification of symbolic computation systems is motivated by the need ... |
Article
Verifying the bridge between simplicial topology and algebra: the Eilenberg–Zilber algorithm
(Oxford Academic, 2013)
The Eilenberg–Zilber algorithm is one of the central components of the computer algebra system called Kenzo, devoted ... |
Presentation
Certified Symbolic Manipulation: Bivariate Simplicial Polynomials
(ACM, 2013)
Certified symbolic manipulation is an emerging new field where programs are accompanied by certificates that, suitably ... |
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
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
Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials
(Springer, 2011)
In this paper we present a complete formalization, using the ACL2 theorem prover, of the Normalization Theorem, a result ... |
Chapter of Book
Topología simplicial en ACL2
(Universidad de la Rioja, 2010)
|
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 ... |
Presentation
ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System
(Springer, 2009)
Kenzo is a Computer Algebra system devoted to Algebraic Topology, and written in the Common Lisp programming language. It ... |
Article
Constructing Formally Verified Reasoners for the ALC Description Logic
(Elsevier, 2008)
Description Logics are a family of logics used to represent and reason about conceptual and terminological knowledge. ... |
Article
Efficient execution in an automated reasoning environment
(Cambridge University Press, 2008)
We describe a method that permits the user of a mechanized mathematical logic to write elegant logical definitions while ... |
Presentation
A Formally Verified Prover for the ALC Description Logic
(Springer, 2007)
The Ontology Web Language (OWL) is a language used for the Semantic Web. OWL is based on Description Logics (DLs), a ... |
Article
Formal Correctness of a Quadratic Unification Algorithm
(Springer, 2006)
We present a case study using ACL2 [5] to verify a non-trivial algorithm that uses efficient data structures. The algorithm ... |
Article
Verification of the Formal Concept Analysis
(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 ... |
Article
Formal verification of a generic framework to synthesize SAT-provers
(Springer, 2004)
We present in this paper an application of the ACL2 system to generate and reason about propositional satis ability provers. ... |
Presentation
Verified Computer Algebra in ACL2 (Gröbner Bases Computation)
(Springer, 2004)
In this paper, we present the formal verification of a Common Lisp implementation of Buchberger’s algorithm for computing Gröbner ... |
Presentation
Formal Reasoning about Efficient Data Structures: A Case Study in ACL2
(Springer, 2003)
We describe in this paper the formal verification, using the ACL2 system, of a syntactic unification algorithm where terms ... |
Presentation
Formal Verification of Molecular Computational Models in ACL2: A Case Study
(Springer, 2003)
Theorem proving is a classical AI problem with a broad range of applications. Since its complexity is exponential in the ... |
Presentation
A Formal Proof of Dickson’s Lemma in ACL2
(Springer, 2003)
Dickson’s Lemma is the main result needed to prove the termination of Buchberger’s algorithm for computing Gr¨obner basis ... |
Presentation
A Generic Instantiation Tool and a Case Study: A Generic Multiset Theory.
(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 ... |
Presentation
Progress Report: Term Dags Using Stobjs
(University of Texas, 2002)
We explore in this paper the use of efficient data structures to implement operations on first-order terms, that can be ... |
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 ... |
Presentation
Verification in ACL2 of a Generic Framework to Synthesize SAT–Provers
(Springer, 2002)
We present in this paper an application of the ACL2 system to reason about propositional satisfiability provers. For that ... |
Presentation
A Theory About First-Order Terms in ACL2
(University of Texas, 2002)
We describe the development in ACL2 of a library of results about first-order terms. In particular, we present the ... |
PhD Thesis
Una teoría computacional acerca de la lógica ecuacional formalización en ACL2 de la lógica ecuacional y demostración automática de sus propiedades
(2001)
El objetivo principal de la Tesis es el desarrollo de una teoría computacional acerca de la lógica ecuacional, usando para ... |
Presentation
Verifying an Applicative ATP Using Multiset Relations
(Springer, 2001)
We present in this paper a formalization of multiset relations in the ACL2 theorem prover [6], and we show how multisets ... |
Presentation
Multiset Relations: A Tool for Proving Termination
(University of Texas, 2000)
|
Presentation
Formalizing Rewriting in the ACL2 Theorem Prover
(Springer, 2000)
We present an application of the ACL2 theorem prover to formalize and reason about rewrite systems theory. This can be ... |
Book
Curso Práctico de Teoría de Conjuntos
(Ediciones La Ñ, 1998)
Todos los que hemos impartido tópicos diversos relativos a la Teoría de Conjuntos, en primer o segundo ciclo universitario, ... |