Mechanical verification of a rule-based unification algorithm in the Boyer-Moore theorem prover. - José-Luis Ruiz-Reina; José-Antonio Alonso; María-José Hidalgo; Francisco-Jesús Martín-Mateos (APPIA-GULP-PRODE, 1999)

Formalizing Rewriting in the ACL2 Theorem Prover. - José-Luis Ruiz-Reina; José-Antonio Alonso; María-José Hidalgo; Francisco-Jesús Martín-Mateos (AISC, 2000)

Verifying an Applicative ATP Using Multiset Relations. - Francisco-Jesús Martín-Mateos; José-Antonio Alonso; María-José Hidalgo; José-Luis Ruiz-Reina (EUROCAST, 2001)

Verification in ACL2 of a Generic Framework to Synthesize SAT-Provers. - Francisco-Jesús Martín-Mateos; José-Antonio Alonso; María-José Hidalgo; José-Luis Ruiz-Reina (LOPSTR, 2002)

Formal Proofs About Rewriting Using ACL2. - José-Luis Ruiz-Reina; José-Antonio Alonso; María-José Hidalgo; Francisco-Jesús Martín-Mateos (Ann. Math. Artif. Intell., 2002)

Formal Verification of Molecular Computational Models in ACL2: A Case Study. - Francisco-Jesús Martín-Mateos; José-Antonio Alonso; María-José Hidalgo; José-Luis Ruiz-Reina (CAEPIA, 2003)

Formal Reasoning about Efficient Data Structures: A Case Study in ACL2. - José-Luis Ruiz-Reina; José Antonio Alonso Jimenez; María-José Hidalgo; Francisco-Jesús Martín-Mateos (LOPSTR, 2003)

A Formal Proof of Dickson's Lemma in ACL2. - Francisco-Jesús Martín-Mateos; José-Antonio Alonso; María-José Hidalgo; José-Luis Ruiz-Reina (LPAR, 2003)

Formal Verification of a Generic Framework to Synthetize SAT-Provers. - Francisco-Jesús Martín-Mateos; José-Antonio Alonso; María-José Hidalgo; José-Luis Ruiz-Reina (J. Autom. Reason., 2004)

Formal Correctness of a Quadratic Unification Algorithm. - José-Luis Ruiz-Reina; Francisco-Jesús Martín-Mateos; José-Antonio Alonso; María-José Hidalgo (J. Autom. Reason., 2006)

A Formally Verified Prover for the ALC Description Logic. - José-Antonio Alonso; Joaquín Borrego-Díaz; María-José Hidalgo; Francisco-Jesús Martín-Mateos; José-Luis Ruiz-Reina (TPHOLs, 2007)

Constructing Formally Verified Reasoners for the ACL Description Logic. - María-José Hidalgo; José-Antonio Alonso; Francisco-Jesús Martín-Mateos; José-Luis Ruiz-Reina (WWV, 2007)

Proof Pearl: a Formal Proof of Higman's Lemma in ACL2. - Francisco-Jesús Martín-Mateos; José-Luis Ruiz-Reina; José-Antonio Alonso; María-José Hidalgo (J. Autom. Reason., 2011)

Formally Verified Tableau-Based Reasoners for a Description Logic. - 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 (J. Autom. Reason., 2014)

A logic-algebraic tool for reasoning with Knowledge-Based Systems. - José A. Alonso-Jiménez; Gonzalo A. Aranda-Corral; Joaquín Borrego-Díaz; María Magdalena Fernández-Lebrón; María-José Hidalgo-Doblado (J. Log. Algebraic Methods Program., 2018)