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 |
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 | 25 | 2002 |
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 |
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 International Conference on Artificial Intelligence and Symbolic Computation …, 2000 | 15 | 2000 |
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 | 12 | 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 |
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 |
Formally verified tableau-based reasoners for a description logic MJ Hidalgo-Doblado, JA Alonso-Jiménez, J Borrego-Díaz, ... Journal of automated reasoning 52 (3), 331-360, 2014 | 8 | 2014 |
Verification of the Formal Concept Analysis. JA Alonso, J Borrego, MJ Hidalgo, FJM Mateos, JLR Reina RACSAM 98 (1), 3-16, 2004 | 7 | 2004 |