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 | 39 | 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 |

Formalizing simplicial topology in ACL2 M Andrés, L Lambán, J Rubio, JL Ruiz-Reina Proceedings of ACL2 Workshop 2007, 34-39, 2007 | 23 | 2007 |

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 | 23 | 2002 |

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 | 19 | 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 |

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 |

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 | 14 | 2000 |

Multiset relations: A tool for proving termination JL Ruiz Reina, JA Alonso Jiménez, MJ Hidalgo Doblado, ... ACL2 Workshop 2000 (2000)., 2000 | 14 | 2000 |

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 | 13 | 2006 |

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 | 12 | 1999 |

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 | 10 | 2011 |

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 | 10 | 2004 |

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 | 10 | 2003 |

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 | 9* | 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 | 9* | 2011 |

A Formally Verified Prover for the Description Logic JA Alonso, J Borrego-Díaz, MJ Hidalgo, FJ Martin-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 (4), 287-313, 2004 | 9 | 2004 |

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 | 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 |