- idUS
- Listar por autor
Listar por autor "Ruiz Reina, José Luis"
Mostrando ítems 21-32 de 32
-
Ponencia
Progress Report: Term Dags Using Stobjs
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 explore in this paper the use of efficient data structures to implement operations on first-order terms, that can be ...
-
Artículo
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
Proving and Computing: Applying Automated Reasoning to the Verification of Symbolic Computation Systems
Ruiz Reina, José Luis (Springer, 2014)The application of automated reasoning to the formal verification of symbolic computation systems is motivated by the ...
-
Tesis Doctoral
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
Ruiz Reina, José Luis (2001)El objetivo principal de la Tesis es el desarrollo de una teoría computacional acerca de la lógica ecuacional, usando para ...
-
Capítulo de Libro
Topología simplicial en ACL2
Lambán Pardo, Laureano; Martín Mateos, Francisco Jesús; Ruiz Reina, José Luis (Universidad de la Rioja, 2010) -
Ponencia
Towards a verifiable topology of data
Lambán Pardo, Laureano; Martín Mateos, Francisco Jesús; Rubio, Julio; Ruiz Reina, José Luis (Universidad de La Rioja, Departamento de Matemáticas y Computación, 2016) -
Ponencia
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 ...
-
Ponencia
Verification in ACL2 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, 2002)We present in this paper an application of the ACL2 system to reason about propositional satisfiability provers. For that ...
-
Artículo
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 ...
-
Ponencia
Verified Computer Algebra in ACL2 (Gröbner Bases Computation)
Medina Bulo, Inmaculada; Palomo Lozano, Francisco; Alonso Jiménez, José Antonio; Ruiz Reina, José Luis (Springer, 2004)In this paper, we present the formal verification of a Common Lisp implementation of Buchberger’s algorithm for ...
-
Ponencia
Verifying an Applicative ATP Using Multiset Relations
Martín Mateos, Francisco Jesús; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Ruiz Reina, José Luis (Springer, 2001)We present in this paper a formalization of multiset relations in the ACL2 theorem prover [6], and we show how multisets ...
-
Artículo
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 ...