| 2008 |
|---|
| 15 | EE | 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) |
| 14 | EE | David A. Greve,
Matt Kaufmann,
Panagiotis Manolios,
J. Strother Moore,
Sandip Ray,
José-Luis Ruiz-Reina,
R. O. B. Sumners,
Daron Vroon,
Matthew Wilding:
Efficient execution in an automated reasoning environment.
J. Funct. Program. 18(1): 15-46 (2008) |
| 2007 |
|---|
| 13 | EE | 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 |
|---|
| 12 | EE | 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 |
|---|
| 11 | EE | 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 |
|---|
| 10 | EE | Inmaculada Medina-Bulo,
Francisco Palomo-Lozano,
José A. Alonso-Jiménez,
José-Luis Ruiz-Reina:
Verified Computer Algebra in Acl2. Gröbner Bases Computation.
AISC 2004: 171-184 |
| 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.
Int. J. Approx. Reasoning 32(4): 287-313 (2004) |
| 2003 |
|---|
| 8 | EE | 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 | EE | José-Luis Ruiz-Reina,
José Antonio Alonso Jimenez,
María-José Hidalgo,
Francisco-Jesús Martín-Mateos:
Formal Reasoning about Efficient Data Structures: A Case Study in ACL2.
LOPSTR 2003: 75-91 |
| 6 | EE | 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 |
|---|
| 5 | EE | 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 |
| 4 | | 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 |
|---|
| 3 | EE | 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 |
|---|
| 2 | EE | 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 |
|---|
| 1 | | 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 |
