 | 2011 |
| 18 |  | Francisco-Jesús Martín-Mateos,
José-Luis Ruiz-Reina,
José-Antonio Alonso,
María-José Hidalgo:
Proof Pearl: a Formal Proof of Higman's Lemma in ACL2.
J. Autom. Reasoning 47(3): 229-250 (2011) |
| 17 |  | Eugenio Roanes-Lozano,
Antonio Hernando,
José-Antonio Alonso,
Luis M. Laita:
A logic approach to decision taking in a railway interlocking system using Maple.
Mathematics and Computers in Simulation 82(1): 15-28 (2011) |
| 2008 |
| 16 |  | María-José Hidalgo,
José-Antonio Alonso,
Francisco-Jesús Martín-Mateos,
José-Luis Ruiz-Reina:
Constructing Formally Verified Reasoners for the ACC Description Logic.
Electr. Notes Theor. Comput. Sci. 200(3): 87-102 (2008) |
| 2007 |
| 15 |  | José-Antonio Alonso,
Joaquín Borrego-Díaz,
María-José Hidalgo,
Francisco-Jesús Martín-Mateos,
José-Luis Ruiz-Reina:
A Formally Verified Prover for the ALC Description Logic.
TPHOLs 2007: 135-150 |
| 2006 |
| 14 |  | José-Antonio Alonso,
Maria Teresa Lamata:
Consistency in the Analytic Hierarchy Process: a New Approach.
International Journal of Uncertainty, Fuzziness and Knowledge-Based Systems 14(4): 445-459 (2006) |
| 13 |  | José-Luis Ruiz-Reina,
Francisco-Jesús Martín-Mateos,
José-Antonio Alonso,
María-José Hidalgo:
Formal Correctness of a Quadratic Unification Algorithm.
J. Autom. Reasoning 37(1-2): 67-92 (2006) |
| 2005 |
| 12 |  | Manuel Palomo,
Francisco-Jesús Martín-Mateos,
José-Antonio Alonso:
Rete Algorithm Applied to Robotic Soccer.
EUROCAST 2005: 571-576 |
| 11 |  | José-Antonio Alonso,
Maria Teresa Lamata:
A Statistical Criterion of Consistency in the Analytic Hierarchy Process.
MDAI 2005: 67-76 |
| 10 |  | Francisco-Jesús Martín-Mateos,
José-Luis Ruiz-Reina,
José-Antonio Alonso,
María-José Hidalgo:
Proof Pearl: A Formal Proof of Higman's Lemma in ACL2.
TPHOLs 2005: 358-372 |
| 2004 |
| 9 |  | Francisco-Jesús Martín-Mateos,
José-Antonio Alonso,
María-José Hidalgo,
José-Luis Ruiz-Reina:
Formal Verification of a Generic Framework to Synthetize SAT-Provers.
J. Autom. Reasoning 32(4): 287-313 (2004) |
| 2003 |
| 8 |  | Francisco-Jesús Martín-Mateos,
José-Antonio Alonso,
María-José Hidalgo,
José-Luis Ruiz-Reina:
Formal Verification of Molecular Computational Models in ACL2: A Case Study.
CAEPIA 2003: 344-353 |
| 7 |  | Francisco-Jesús Martín-Mateos,
José-Antonio Alonso,
María-José Hidalgo,
José-Luis Ruiz-Reina:
A Formal Proof of Dickson's Lemma in ACL2.
LPAR 2003: 49-58 |
| 2002 |
| 6 |  | Francisco-Jesús Martín-Mateos,
José-Antonio Alonso,
María-José Hidalgo,
José-Luis Ruiz-Reina:
Verification in ACL2 of a Generic Framework to Synthesize SAT-Provers.
LOPSTR 2002: 182-198 |
| 5 |  | José-Luis Ruiz-Reina,
José-Antonio Alonso,
María-José Hidalgo,
Francisco-Jesús Martín-Mateos:
Formal Proofs About Rewriting Using ACL2.
Ann. Math. Artif. Intell. 36(3): 239-262 (2002) |
| 2001 |
| 4 |  | Francisco-Jesús Martín-Mateos,
José-Antonio Alonso,
María-José Hidalgo,
José-Luis Ruiz-Reina:
Verifying an Applicative ATP Using Multiset Relations.
EUROCAST 2001: 612-626 |
| 2000 |
| 3 |  | José-Luis Ruiz-Reina,
José-Antonio Alonso,
María-José Hidalgo,
Francisco-Jesús Martín-Mateos:
Formalizing Rewriting in the ACL2 Theorem Prover.
AISC 2000: 92-106 |
| 1999 |
| 2 |  | José-Luis Ruiz-Reina,
José-Antonio Alonso,
María-José Hidalgo,
Francisco-Jesús Martín-Mateos:
Mechanical verification of a rule-based unification algorithm in the Boyer-Moore theorem prover.
APPIA-GULP-PRODE 1999: 289-304 |
| 1 |  | Luis M. Laita,
Eugenio Roanes-Lozano,
Luis de Ledesma,
José-Antonio Alonso:
A computer algebra approach to verification and deduction in many-valued knowledge systems.
Soft Comput. 3(1): 7-19 (1999) |