 | 2011 |
|---|
| 14 |       | 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) |
| 2008 |
|---|
| 13 | | 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 |
|---|
| 12 | | 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 |
|---|
| 11 | | 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 |
|---|
| 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 | | 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 | | 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 | | 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 | | 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 | | 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 |
Data released under the ODC-BY 1.0 license — See also our legal information page