| 2008 |
|---|
| 16 | 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) |
| 2007 |
|---|
| 15 | 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 |
|---|
| 14 | EE | José A. Alonso-Jiménez,
Joaquín Borrego-Díaz,
Antonia M. Chávez-González,
Francisco-Jesús Martín-Mateos:
Foundational Challenges in Automated Semantic Web Data and Ontology Cleaning.
IEEE Intelligent Systems 21(1): 42-52 (2006) |
| 13 | 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 |
|---|
| 12 | EE | Manuel Palomo,
Francisco-Jesús Martín-Mateos,
José-Antonio Alonso:
Rete Algorithm Applied to Robotic Soccer.
EUROCAST 2005: 571-576 |
| 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 | | 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 |
|---|
| 9 | 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 |
| 8 | 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 |
| 7 | 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 |
|---|
| 6 | 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 |
| 5 | EE | Carmen Graciani Díaz,
Francisco-Jesús Martín-Mateos,
Mario J. Pérez-Jiménez:
Specification of Adleman's Restricted Model Using an Automated Reasoning System: Verification of Lipton's Experiment.
UMC 2002: 126-136 |
| 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 |
