José-Luis Ruiz-Reina

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