| 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 | 43 | 2008 |
| A Generic Instantiation Tool and a Case Study: A Generic Multiset Theory. FJ Martín Mateos, JA Alonso Jiménez, MJ Hidalgo Doblado, ... ACL2 2002: Third International Workshop on the ACL2 Theorem Prover and Its …, 2002 | 25 | 2002 |
| Formal proofs about rewriting using ACL2 JL Ruiz-Reina, JA Alonso, MJ Hidalgo, FJ Martín-Mateos Annals of Mathematics and Artificial Intelligence 36, 239-262, 2002 | 24 | 2002 |
| Formalizing simplicial topology in ACL2 M Andrés, L Lambán, J Rubio, JL Ruiz-Reina Proceedings ACL2 Workshop, 34-39, 2007 | 23 | 2007 |
| 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 | 21 | 2010 |
| 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 | 18 | 2009 |
| Formalizing rewriting in the ACL2 theorem prover JL Ruiz-Reina, JA Alonso, MJ Hidalgo, FJ Martín-Mateos Artificial Intelligence and Symbolic Computation: International Conference …, 2001 | 15 | 2001 |
| 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 | 14 | 2012 |
| Formal correctness of a quadratic unification algorithm JL Ruiz-Reina, FJ Martín-Mateos, JA Alonso, MJ Hidalgo Journal of Automated Reasoning 37 (1), 67-92, 2006 | 14 | 2006 |
| Multiset relations: A tool for proving termination JL Ruiz Reina, JA Alonso Jiménez, MJ Hidalgo Doblado, ... ACL2 Workshop 2000 (2000)., 2000 | 14 | 2000 |
| A formal proof of Dickson’s Lemma in ACL2 FJ Martın-Mateos, JA Alonso, MJ Hidalgo, JL Ruiz-Reina Logic for Programming, Artificial Intelligence, and Reasoning: 10th …, 2003 | 13 | 2003 |
| 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 | 13 | 1999 |
| 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 | 11 | 2014 |
| 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 | 11 | 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, 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, 229-250, 2011 | 10* | 2011 |
| Verified Computer Algebra in Acl2 I Medina-Bulo, F Palomo-Lozano, JA Alonso-Jiménez, JL Ruiz-Reina Artificial Intelligence and Symbolic Computation: 7th International …, 2004 | 10 | 2004 |
| 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 | 9 | 2007 |
| 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, 287-313, 2004 | 9 | 2004 |
| Verification of the Formal Concept Analysis. JA Alonso, J Borrego, MJ Hidalgo, FJM Mateos, JLR Reina RACSAM 98 (1), 3-16, 2004 | 7 | 2004 |
Francisco Jesús Martín MateosUniversidad de SevillaVerified email at us.es
