José-Luis Ruiz-Reina

Publication Activity (10 Years)

Years Active: 1999-2017
Publications (10 Years): 1

Top Topics

Relational Database Theory

Automated Reasoning

Top Venues

Ann. Math. Artif. Intell.

Publications

Laureano Lambán, Francisco J. Martín-Mateos, Julio Rubio, José-Luis Ruiz-Reina
Using Abstract Stobjs in ACL2 to Compute Matrix Normal Forms. ITP (2017)
Laureano Lambán, Julio Rubio, Francisco-Jesús Martín-Mateos, José-Luis Ruiz-Reina
Verifying the bridge between simplicial topology and algebra: the Eilenberg-Zilber algorithm. Log. J. IGPL 22 (1) (2014)
José-Luis Ruiz-Reina
Proving and Computing: Applying Automated Reasoning to the Verification of Symbolic Computation Systems (Invited Talk). AISC (2014)
María-José Hidalgo-Doblado, José A. Alonso-Jiménez, Joaquín Borrego-Díaz, Francisco-Jesús Martín-Mateos, José-Luis Ruiz-Reina
Formally Verified Tableau-Based Reasoners for a Description Logic. J. Autom. Reason. 52 (3) (2014)
Laureano Lambán, Francisco-Jesús Martín-Mateos, Julio Rubio, José-Luis Ruiz-Reina
Certified symbolic manipulation: bivariate simplicial polynomials. ISSAC (2013)
Laureano Lambán, Francisco-Jesús Martín-Mateos, Julio Rubio, José-Luis Ruiz-Reina
Formalization of a normalization theorem in simplicial topology. Ann. Math. Artif. Intell. 64 (1) (2012)
Laureano Lambán, Francisco-Jesús Martín-Mateos, Julio Rubio, José-Luis Ruiz-Reina
Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials. ITP (2011)
Francisco-Jesús Martín-Mateos, José-Luis Ruiz-Reina, José-Antonio Alonso, María-José Hidalgo
Proof Pearl: a Formal Proof of Higman's Lemma in ACL2. J. Autom. Reason. 47 (3) (2011)
Inmaculada Medina-Bulo, Francisco Palomo-Lozano, José-Luis Ruiz-Reina
A verified Common Lisp implementation of Buchberger's algorithm in ACL2. J. Symb. Comput. 45 (1) (2010)
Francisco-Jesús Martín-Mateos, Julio Rubio, José-Luis Ruiz-Reina
ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System. Calculemus/MKM (2009)
David A. Greve, Matt Kaufmann, Panagiotis Manolios, J Strother Moore, Sandip Ray, José-Luis Ruiz-Reina, Rob Sumners, Daron Vroon, Matthew Wilding
Efficient execution in an automated reasoning environment. J. Funct. Program. 18 (1) (2008)
María-José Hidalgo, José-Antonio Alonso, Francisco-Jesús Martín-Mateos, José-Luis Ruiz-Reina
Constructing Formally Verified Reasoners for the ACL Description Logic. Electron. Notes Theor. Comput. Sci. 200 (3) (2008)
José-Antonio Alonso, Joaquín Borrego-Díaz, María-José Hidalgo, Francisco-Jesús Martín-Mateos, José-Luis Ruiz-Reina
Description Logic. TPHOLs (2007)
José-Luis Ruiz-Reina, Francisco-Jesús Martín-Mateos, José-Antonio Alonso, María-José Hidalgo
Formal Correctness of a Quadratic Unification Algorithm. J. Autom. Reason. 37 (1-2) (2006)
Francisco-Jesús Martín-Mateos, José-Luis Ruiz-Reina, José-Antonio Alonso, María-José Hidalgo
Proof Pearl: A Formal Proof of Higman's Lemma in ACL2. TPHOLs (2005)
Inmaculada Medina-Bulo, Francisco Palomo-Lozano, José A. Alonso-Jiménez, José-Luis Ruiz-Reina
Verified Computer Algebra in Acl2. Gröbner Bases Computation. AISC (2004)
Francisco-Jesús Martín-Mateos, José-Antonio Alonso, María-José Hidalgo, José-Luis Ruiz-Reina
Formal Verification of a Generic Framework to Synthetize SAT-Provers. J. Autom. Reason. 32 (4) (2004)
José-Luis Ruiz-Reina, José Antonio Alonso Jimenez, María-José Hidalgo, Francisco-Jesús Martín-Mateos
Formal Reasoning about Efficient Data Structures: A Case Study in ACL2. LOPSTR (2003)
Francisco-Jesús Martín-Mateos, José-Antonio Alonso, María-José Hidalgo, José-Luis Ruiz-Reina
A Formal Proof of Dickson's Lemma in ACL2. LPAR (2003)
Francisco-Jesús Martín-Mateos, José-Antonio Alonso, María-José Hidalgo, José-Luis Ruiz-Reina
Formal Verification of Molecular Computational Models in ACL2: A Case Study. CAEPIA (2003)
Francisco-Jesús Martín-Mateos, José-Antonio Alonso, María-José Hidalgo, José-Luis Ruiz-Reina
Verification in ACL2 of a Generic Framework to Synthesize SAT-Provers. LOPSTR (2002)
José-Luis Ruiz-Reina, José-Antonio Alonso, María-José Hidalgo, Francisco-Jesús Martín-Mateos
Formal Proofs About Rewriting Using ACL2. Ann. Math. Artif. Intell. 36 (3) (2002)
Francisco-Jesús Martín-Mateos, José-Antonio Alonso, María-José Hidalgo, José-Luis Ruiz-Reina
Verifying an Applicative ATP Using Multiset Relations. EUROCAST (2001)
José-Luis Ruiz-Reina, José-Antonio Alonso, María-José Hidalgo, Francisco-Jesús Martín-Mateos
Formalizing Rewriting in the ACL2 Theorem Prover. AISC (2000)
José-Luis Ruiz-Reina, José-Antonio Alonso, María-José Hidalgo, Francisco-Jesús Martín-Mateos
Mechanical verification of a rule-based unification algorithm in the Boyer-Moore theorem prover. APPIA-GULP-PRODE (1999)