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)

A computer algebra approach to verification and deduction in many-valued knowledge systems. - Luis M. Laita; Eugenio Roanes-Lozano; Luis de Ledesma; José-Antonio Alonso (Soft Comput., 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)

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)

Rete Algorithm Applied to Robotic Soccer. - Manuel Palomo-Duarte; Francisco-Jesús Martín-Mateos; José-Antonio Alonso (EUROCAST, 2005)

A Statistical Criterion of Consistency in the Analytic Hierarchy Process. - José-Antonio Alonso; María Teresa Lamata (MDAI, 2005)

Consistency in the Analytic Hierarchy Process: a New Approach. - José-Antonio Alonso; M. Teresa Lamata (Int. J. Uncertain. Fuzziness Knowl. Based Syst., 2006)

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)

KRRT: Knowledge Representation and Reasoning Tutor System. - José-Antonio Alonso; Gonzalo A. Aranda-Corral; Francisco J. Martín-Mateos (EUROCAST, 2007)

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)

A logic approach to decision taking in a railway interlocking system using Maple. - Eugenio Roanes-Lozano; Antonio Hernando; José-Antonio Alonso; Luis M. Laita (Math. Comput. Simul., 2011)

Revisiting four-valued logics from Maple using the Logics Explorer package. - Eugenio Roanes-Lozano; José-Antonio Alonso; Antonio Hernando (Math. Comput. Simul., 2014)