José-Luis Ruiz-Reina
José-Luis Ruiz-Reina
Professor of Computer Science, University of Seville (Spain)
Verified email at us.es
Title
Cited by
Cited by
Year
Efficient execution in an automated reasoning environment
DA Greve, M Kaufmann, P Manolios, JS Moore, S Ray, JL Ruiz Reina, ...
Journal of Functional Programming, 18 (1), 15-46., 2008
392008
A generic instantiation tool and a case study: A generic multiset theory
FJ Martın-Mateos, JA Alonso, MJ Hidalgo, JL Ruiz-Reina
Proc. 3rd International Workshop on the ACL2 Theorem Prover and its …, 2002
252002
Formalizing simplicial topology in ACL2
M Andrés, L Lambán, J Rubio, JL Ruiz-Reina
Proceedings ACL2 Workshop, 34-39, 2007
232007
Formal proofs about rewriting using ACL2
JL Ruiz-Reina, JA Alonso, MJ Hidalgo, FJ Martín-Mateos
Annals of Mathematics and Artificial Intelligence 36 (3), 239-262, 2002
222002
A verified Common Lisp implementation of Buchberger’s algorithm in ACL2
I Medina-Bulo, F Palomo-Lozano, JL Ruiz-Reina
Journal of Symbolic Computation 45 (1), 96-123, 2010
192010
ACL2 verification of simplicial degeneracy programs in the Kenzo system
FJ Martín-Mateos, J Rubio, JL Ruiz-Reina
International Conference on Intelligent Computer Mathematics, 106-121, 2009
182009
Formalization of a normalization theorem in simplicial topology
L Lambán, FJ Martín–Mateos, J Rubio, JL Ruiz–Reina
Annals of Mathematics and Artificial Intelligence 64 (1), 1-37, 2012
142012
Formal correctness of a quadratic unification algorithm
JL Ruiz-Reina, FJ Martín-Mateos, JA Alonso, MJ Hidalgo
Journal of Automated Reasoning 37 (1-2), 67-92, 2006
142006
Multiset relations: A tool for proving termination
JL Ruiz-Reina, JA Alonso, MJ Hidalgo, FJ Martin
In ACL2 Workshop, 2000
142000
Mechanical verification of a rule-based unification algorithm in the Boyer-Moore theorem prover.
JL Ruiz-Reina, JA Alonso, MJ Hidalgo, FJ Martín-Mateos
APPIA-GULP-PRODE, 289-304, 1999
141999
Formalizing rewriting in the ACL2 theorem prover
JL Ruiz-Reina, JA Alonso, MJ Hidalgo, FJ Martín-Mateos
International Conference on Artificial Intelligence and Symbolic Computation …, 2000
132000
A formal proof of Dickson’s Lemma in ACL2
FJ Martın-Mateos, JA Alonso, MJ Hidalgo, JL Ruiz-Reina
International Conference on Logic for Programming Artificial Intelligence …, 2003
112003
Proof pearl: A formal proof of Higman’s lemma in ACL2
FJ Martín-Mateos, JL Ruiz-Reina, JA Alonso, MJ Hidalgo
Journal of Automated Reasoning 47 (3), 229-250, 2011
10*2011
Proof pearl: A formal proof of Higman’s lemma in ACL2
FJ Martín-Mateos, JL Ruiz-Reina, JA Alonso, MJ Hidalgo
Journal of Automated Reasoning 47 (3), 229-250, 2011
10*2011
Applying ACL2 to the formalization of algebraic topology: simplicial polynomials
L Lambán, FJ Martín-Mateos, J Rubio, JL Ruiz-Reina
International Conference on Interactive Theorem Proving, 200-215, 2011
102011
A Formally Verified Prover for the Description Logic
JA Alonso, J Borrego-Díaz, MJ Hidalgo, FJ Martín-Mateos, JL Ruiz-Reina
International Conference on Theorem Proving in Higher Order Logics, 135-150, 2007
92007
Verifying the bridge between simplicial topology and algebra: the Eilenberg–Zilber algorithm
L Lambán, J Rubio, FJ Martín-Mateos, JL Ruiz-Reina
Logic Journal of IGPL 22 (1), 39-65, 2014
82014
Formal verification of a generic framework to synthesize SAT-provers
FJ Martín-Mateos, JA Alonso, MJ Hidalgo, JL Ruiz-Reina
Journal of Automated Reasoning 32 (4), 287, 2004
82004
Verified Computer Algebra in Acl2
I Medina-Bulo, F Palomo-Lozano, JA Alonso-Jiménez, JL Ruiz-Reina
International Conference on Artificial Intelligence and Symbolic Computation …, 2004
82004
Verification of the Formal Concept Analysis.
JA Alonso, J Borrego, MJ Hidalgo, FJM Mateos, JLR Reina
RACSAM 98 (1), 3-16, 2004
72004
The system can't perform the operation now. Try again later.
Articles 1–20