RUIZ REINA, JOSE LUIS

Perfil en ORCID: 0000-0003-1021-3256

Perfil en ResearcherID: N-8053-2015

Perfil en Scopus: 6603160771\

Perfil en Dialnet: 1012617

Grupos de Investigación

• LOGICA, COMPUTACION E INGENIERIA DEL CONOCIMIENTO

Responsable de los siguientes proyectos/ayudas en la US

Proyectos:

• GESTIÓN MECANIZADA DEL CONOCIMIENTO MATEMÁTICO. APLICACIONES EN LÓGICA ( MTM2009-13842-C02-02 ).

Participa los siguientes proyectos/ayudas en la US

Proyectos:

• Lógica Computacional para la Ciencia del Dato ( TIN2013-41086-P - Investigador/a).
• Lógica Computacional para la Ciencia del Dato ( TIN2013-41086-P - Investigador/a).
• GESTIÓN MECANIZADA DEL CONOCIMIENTO MATEMÁTICO. LOS CASOS DE LA TOPOLOGÍA ALGEBRAICA Y LA LÓGICA ( MTM2009-13842-C02-01 - Investigador/a).
• SISTEMAS VERIFICADOS PARA RAZONAMIENTO EN LA WEB SEMÁNTICA ( TIN2004-03884 - Investigador/a).
• DESARROLLO Y VERIFICACIÓN FORMAL DE SISTEMAS DE RAZONAMIENTO ( TIC2000-1368-C03-02 - Investigador/a).
• VERIFICACIÓN DE BASES DE CONOCIMIENTO Y SISTEMAS DE RAZONAMIENTO ( PB96-0098-C04-04 - Investigador/a).

Contratos:

• SISTEMAS DE ENSEÑANZA ASISTIDA POR ORDENADOR EN EL PROYECTO ATLAS ( CICYT 95-0350 - Investigador/a ).

Publicaciones

Libros:

• Medina-Bulo, María Inmaculada, Alonso-Jimenez, Jose Antonio, Ruiz-Reina, Jose Luis:
  VERIFICACIÓN FORMAL EN ACL2 DEL ALGORITMO DE BUCHBERGER. PROQUEST INFORMATION AND LEARNING. 2004. ISBN
• Ruiz-Reina, Jose Luis:
  CURSO PRÁCTICO DE TEORÍA DE CONJUNTOS. LA Ñ. 1998. ISBN 84-89524-45-9
• Alonso-Jimenez, Jose Antonio, Borrego-Diaz, Joaquin, Pérez-Jiménez, Mario Jesús, Ruiz-Reina, Jose Luis:
  Curso práctico de Teoría de Conjuntos. EDICIONES LA Ñ. 1998. ISBN 84-89524-45-9 94152 2
• Ruiz-Reina, Jose Luis:
  SISTEMA DE REESCRITURA. . . ISBN

Capítulo de Libros:

• Lambán-Pardo, Laureano, Martín-mateos, Francisco Jesús, Ruiz-Reina, Jose Luis:
  TOPOLOGÍA SIMPLICIAL EN ACL2. Pag. 1 - 20. En: CONTRIBUCIONES CIENTÍFICAS EN HONOR DE MIRIAN ANDRÉS GÓMEZ. UNIVERSIDAD DE LA RIOJA. 2010. ISBN 978-84-96487-50-5
• Martín-mateos, Francisco Jesús, Ruiz-Reina, Jose Luis, Rubio-García, Julio, Lambán-Pardo, Laureano:
  VERIFICACIÓN Y EFICIENCIA EN PROGRAMAS PARA EL CÁLCULO SIMBÓLICO: ESTUDIO DE UN CASO. Pag. 7 - 14. En: IX JORNADAS SOBRE PROGRAMACIÓN Y LENGUAJES. . 2009. ISBN 978-84-692-4600-9
• Ruiz-Reina, Jose Luis, Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Martín-mateos, Francisco Jesús:
  TERMINATION IN ACL2 USING MULTISET RELATION. Pag. 217 - 245. En: THIRTY FIVE YEARS OF AUTOMATING MATHEMATICS. KLUWER ACADEMIC PUBLISHERS. 2003. ISBN 1-4020-1656-5
• Martín-mateos, Francisco Jesús, Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Ruiz-Reina, Jose Luis:
  FORMAL VERIFICATION OF MOLECULAR COMPUTATIONAL MODELS IN ACL2: A CASE STUDY. Pag. 235 - 244. En: CAEPIA-TTIA 2003. UNIVERSIDAD DEL PAÍS VASCO. 2003. ISBN 84-8373-564-4
• Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Martín-mateos, Francisco Jesús, Ruiz-Reina, Jose Luis:
  FORMALIZACIÓN DEL RAZONAMIENTO ECUACIONAL EN UNA LÓGICA COMPUTACIONAL. Pag. 41 - 50. En: ACTAS DEL ENCUENTRO DE MATEMÁTICOS ANDALUCES. SECRETARIADO DE PUBLICACIONES - UNIVERSIDAD DE SEVILLA. 2001. ISBN 84-472-0290-9
• Ruiz-Reina, Jose Luis, Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose:
  FORMALIZING REWRITING IN THE ACL2 THEOREM PROVER. Pag. 92 - 106. En: 5TH INTERNATIONAL CONFERENCE ON ARTIFICIAL INTELLIGENCE AND SYMBOLIC COMPUTATION. . 2000. ISBN 3-540-42071-1
• Martín-mateos, Francisco Jesús, Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Ruiz-Reina, Jose Luis:
  RAZONAMIENTO AUTOMÁTICO EN SISTEMAS DE REPRESENTACIÓN DEL CONOCIMIENTO (Y SU RELACIÓN CON LA ENSEÑANZA DE LA INTELIGENCIA ARTIFICIAL). Pag. 289 - 296. En: IV JORNADES SOBRE L'ENSENYAMENT UNIVERSITARI DE LA INFORMATICA (JENUI 98). ENGINYERIA I ARQUITECTURA LA SALLE. 1998. ISBN 84-922538-3-5
• Ruiz-Reina, Jose Luis, Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Martín-mateos, Francisco Jesús:
  VERIFICACIÓN AUTOMÁTICA DE SISTEMAS DE RAZONAMIENTO (APLICACIÓN A LA ENSEÑANZA DE LA INTELIGENCIA ARTIFICIAL). Pag. 297 - 304. En: IV JORNADES SOBRE L'ENSENYAMENT UNIVERSITARI DE LA INFORMATICA (JENUI 98). ENGINYERIA I ARQUITECTURA LA SALLE. 1998. ISBN 84-922538-3-5
• Arrabal-Parrilla, Juan Jose, Balbontin-Noval, Delia, Alonso-Jimenez, Jose Antonio, Lara-Martin, Francisco Felix, Martín-mateos, Francisco Jesús, Pérez-Jiménez, Mario Jesús, Ruiz-Reina, Jose Luis:
  GTI: UNA HERRAMIENTA DE EDICIÓN DE CURSOS ADAPTATIVOS. Pag. 627 - 634. En: ACTAS DEL XIII CONGRESO NACIONAL DE INGENIERÍA DE PROYECTOS. ANTONIO F. MARTIN NAVARRO. 1997. ISBN 84-88783-30-2
• Ruiz-Reina, Jose Luis, Gegúndez-Arias, Manuel Emilio:
  PRUEBA POR CONSISTENCIA DE TEOREMAS INDUCTIVOS: INDUCCIÓN SIN SINDUCCIÓN. Pag. 597 - 606. En: LENGUAJES NATURALES Y LENGUAJES FORMALES, X. Promociones Y Publicaciones Universitarias. 1994. ISBN 84-477-0396-7

Publicaciones en Revistas:

• Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Borrego-Diaz, Joaquin, Martín-mateos, Francisco Jesús, Ruiz-Reina, Jose Luis:
  FORMALLY VERIFIED TABLEAU-BASED REASONERS FOR A DESCRIPTION LOGIC. En: Journal of Automated Reasoning. 2014. Vol. 52. Núm. 3. Pag. 331-360 10.1007/s10817-013-9291-8
• Lamban, Laureano, Rubio, Julio, Martín-mateos, Francisco Jesús, Ruiz-Reina, Jose Luis:
  VERIFYING THE BRIDGE BETWEEN SIMPLICIAL TOPOLOGY AND ALGEBRA: THE EILENBERG¿ZILBER ALGORITHM. En: Interest Group in Pure and Applied Logics. Logic Journal. 2014. Vol. 22. Núm. 1. Pag. 39-65 10.1093/jigpal/jzt034
• Ruiz-Reina, Jose Luis:
  Proving and Computing: Applying Automated Reasoning to the Verification of Symbolic Computation Systems (Invited Talk). En: Lecture Notes in Computer Science. 2014. Vol. 8884. Núm. . Pag. 1-6 10.1007/978-3-319-13770-4_1
• Lambán-Pardo, Laureano, Martín-mateos, Francisco Jesús, Rubio-García, Julio, Ruiz-Reina, Jose Luis:
  FORMALIZATION OF A NORMALIZATION THEOREM IN SIMPLICIAL TOPOLOGY. En: Annals of Mathematics and Artificial Intelligence. 2012. Vol. 64. Núm. 1. Pag. 1-37 10.1007/s10472-011-9274-6
• Lambán-Pardo, Laureano, Martín-mateos, Francisco Jesús, Rubio-García, Julio, Ruiz-Reina, Jose Luis:
  APPLYING ACL2 TO THE FORMALIZATION OF ALGEBRAIC TOPOLOGY: SIMPLICIAL POLYNOMIALS. En: Lecture Notes in Computer Science. 2011. Vol. 6898. Núm. . Pag. 200-215
• Martín-mateos, Francisco Jesús, Ruiz-Reina, Jose Luis, Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose:
  PROOF PEARL: A FORMAL PROOF OF HIGMAN'S LEMMA IN ACL2. En: Journal of Automated Reasoning. 2011. Vol. 47. Núm. 3. Pag. 229-250 10.1007/s10817-010-9178-x
• Lambán-Pardo, Laureano, Martín-mateos, Francisco Jesús, Rubio-García, Julio, Ruiz-Reina, Jose Luis:
  Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials. En: Lecture Notes in Computer Science. 2011. Vol. 6898. Núm. . Pag. 200-215
• Medina-Bulo, María Inmaculada, Palomo-Lozano, Francisco, Ruiz-Reina, Jose Luis:
  A VERIFIED COMMON LISP IMPLEMENTATION OF BUCHBERGER'S ALGORITHM IN ACL2. En: Journal of Symbolic Computation. 2010. Vol. 45. Núm. 1. Pag. 96-123
• Martín-mateos, Francisco Jesús, Rubio-García, Julio, Ruiz-Reina, Jose Luis:
  ACL2 VERIFICATION OF SIMPLICIAL DEGENERACY PROGRAMS IN THE KENZO SYSTEM. En: Lecture Notes in Computer Science. 2009. Vol. 5625. Núm. . Pag. 106-121
• Ruiz-Reina, Jose Luis, Greve-,David A., Kaufmann-,Matt, Manolios-,Panagiotis, Moore-,J Stroother, Ray-,Sandip, Sumners-,Rob, Vroon-,Daron, Wilding-,Matthew:
  EFFICIENT EXECUTION IN AN AUTOMATED REASONING ENVIRONMENT. En: Journal of Functional Programming. 2008. Vol. 18. Núm. 1. Pag. 15-46
• Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Martin-Mateos, Francisco Jesus, Ruiz-Reina, Jose Luis:
  CONSTRUCTING FORMALLY VERIFIED REASONERS FOR THE ALC DESCRIPTION LOGIC. En: Electronic Notes in Theoretical Computer Science. 2008. Vol. 200. Núm. 3. Pag. 87-102
• Alonso-Jimenez, Jose Antonio, Borrego-Diaz, Joaquin, Hidalgo-Doblado, Maria Jose, Martín-mateos, Francisco Jesús, Ruiz-Reina, Jose Luis:
  A FORMALLY VERIFIED PROVER FOR THE ALC DESCRIPTION LOGIC. En: Lecture Notes in Computer Science. 2007. Vol. 4732. Núm. . Pag. 135-150
• Ruiz-Reina, Jose Luis, Martin-Mateos, Francisco Jesus, Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose:
  FORMAL CORRECTNESS OF A QUADRATIC UNIFICATION ALGORITHM. En: Journal of Automated Reasoning. 2006. Vol. 37. Núm. 1-2. Pag. 67-92
• Martin-Mateos, Francisco Jesus, Ruiz-Reina, Jose Luis, Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose:
  PROOF PEARL: A FORMAL PROOF OF HIGMAN S LEMMA IN ACL2. En: Lecture Notes in Computer Science. 2005. Vol. 3603. Núm. . Pag. 358-372
• Martin-Mateos, Francisco Jesus, Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Ruiz-Reina, Jose Luis:
  FORMAL VERIFICATION OF A GENERIC FRAMEWORK TO SYNTHESIZE SAT-PROVERS. En: Journal of Automated Reasoning. 2004. Vol. 32. Núm. 4. Pag. 287-313
• Medina-Bulo, María Inmaculada, Palomo-Lozano, Francisco, Alonso-Jimenez, Jose Antonio, Ruiz-Reina, Jose Luis:
  VERIFIED COMPUTER ALGEBRA IN ACL2 (GROBNER BASES COMPUTATION). En: Lecture Notes in Computer Science. 2004. Vol. 3249. Núm. . Pag. 171-184
• Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Martin-Mateos, Francisco Jesus, Ruiz-Reina, Jose Luis:
  VERIFICATION OF THE FORMAL CONCEPT ANALYSIS. En: Revista de la Real Academia de Ciencias Exactas, Físicas y Naturales - Serie A: Matemáticas. 2004. Vol. 98. Núm. 1-2. Pag. 3-16
• Ruiz-Reina, Jose Luis, Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Martin-Mateos, Francisco Jesus:
  FORMAL REASONING ABOUT EFFICIENT DATA STRUCTURES: A CASE STUDY IN ACL2. En: Lecture Notes in Computer Science. 2004. Vol. 3018. Núm. . Pag. 75-91
• Martin-Mateos, Francisco Jesus, Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Ruiz-Reina, Jose Luis:
  FORMAL VERIFICATION OF MOLECULAR COMPUTATIONAL MODELS IN ACL2: A CASE STUDY. En: Lecture Notes in Computer Science. 2004. Vol. 3040. Núm. . Pag. 344-353
• Martin-Mateos, Francisco Jesus, Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Ruiz-Reina, Jose Luis:
  A FORMAL PROOF OF DICKSON'S LEMMA IN ACL2. En: Lecture Notes in Computer Science. 2003. Vol. 2850. Núm. . Pag. 49-58
• Martin-Mateos, Francisco Jesus, Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Ruiz-Reina, Jose Luis:
  VERIFICATION IN ACL2 OF A GENERIC FRAMEWORK TO SYNTHESIZE SAT-PROVERS. En: Lecture Notes in Computer Science. 2003. Vol. 2664. Núm. . Pag. 182-198
• Ruiz-Reina, Jose Luis, Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Martin-Mateos, Francisco Jesus:
  FORMAL PROOFS ABOUT REWRITING USING ACL2. En: Annals of Mathematics and Artificial Intelligence. 2002. Vol. 36. Núm. 3. Pag. 239-262
• Ruiz-Reina, Jose Luis, Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Martin-Mateos, Francisco Jesus:
  FORMALIZING REWRITING IN THE ACL2 THEOREM PROVER. En: Lecture Notes in Computer Science. 2001. Vol. 1930. Núm. . Pag. 92-106
• Martin-Mateos, Francisco Jesus, Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Ruiz-Reina, Jose Luis:
  VERIFYING AN APPLICATIVE ATP USING MULTISET RELATIONS. En: Lecture Notes in Computer Science. 2001. Vol. 2178. Núm. . Pag. 612-626

Otra participación en Libros de Actas:

• Borrego-Diaz, Joaquin, Ruiz-Reina, Jose Luis, Alonso-Jimenez,Jose A:
  IDEIA 2002: I TALLER IBEROAMERICANO SOBRE DEDUCCIÓN AUTOMÁTICA E INTELIGENCIA ARTIFICIAL. 2002. ISBN . DEPARTAMENTO DE CIENCIAS DE LA COMPUTACION E INTELIGENCIA ARTIFICIAL. UNIVERSIDAD DE SEVILLA Santander (ESPAÑA)

Aportaciones a Congresos:

• Lamban, Laureano, Martín-mateos, Francisco Jesús, Ruiz-Reina, Jose Luis:
  USING ABSTRACT STOBJS IN ACL2 TO COMPUTE MATRIX NORMAL FORMS. Comunicación en congreso. INTERACTIVE THEOREM PROVING. BRASILIA. 2017
• Lambán, Laureano, Martín-mateos, Francisco Jesús, Rubio, Julio, Ruiz-Reina, Jose Luis:
  Towards a Verifiable Topology of Data. Comunicación en congreso. XV Encuentro de Algebra Computacional y Aplicaciones. LOGROÑO (ESPAÑA). 2016
• Pro, José Luis, Ruiz-Reina, Jose Luis, Martín-mateos, Francisco Jesús:
  Formalization in ACL2 of Matrix Algebra Basic Concepts. Comunicación en congreso. European Symposium on Computational Intelligence and Mathematics. - CÁDIZ, - CÁDIZ, ESPAÑA. 2015
• Ruiz-Reina, Jose Luis:
  Proving and Computing: Applying Automated Reasoning to the Verification of Symbolic Computation Systems (Invited Talk). Conferencias impartidas en Congreso. 12th International Conference and Symbolic Computation. Seville, Spain. 2014
• Lamban, Laureano, Martín-mateos, Francisco Jesús, Rubio, Julio, Ruiz-Reina, Jose Luis:
  CERTIFIED SYMBOLIC MANIPULATION: BIVARIATE SIMPLICIAL POLYNOMIALS. Comunicación en congreso. INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND ALGEBRAIC COMPUTATION. BOSTON, USA. 2013
• Lambán-Pardo, Laureano, Martín-mateos, Francisco Jesús, Rubio-García, Julio, Ruiz-Reina, Jose Luis:
  APPLYING ACL2 TO THE FORMALIZATION OF ALGEBRAIC TOPOLOGY: SIMPLICIAL POLYNOMIALS. Comunicación en congreso. INTERACTIVE THEOREM PROVING. NIJMEGEN, PAISES BAJOS. 2011
• Martín-mateos, Francisco Jesús, Ruiz-Reina, Jose Luis, Lambán-Pardo, Laureano:
  FORMALIZING MATHEMATICAL ABSTRACT CONCEPTS IN ACL2. Comunicación en congreso. ALGEBRAIC COMPUTING, SOFT COMPUTING AND PROGRAM VERIFICATION. CASTRO URDIALES. 2010
• Martín-mateos, Francisco Jesús, Ruiz-Reina, Jose Luis, Lambán-Pardo, Laureano:
  POLINOMIOS SIMPLICIALES: UNA HERRAMIENTA PARA LA FORMALIZACIÓN DE LA TOPOLOGÍA SIMPLICIAL EN ACL2. Comunicación en congreso. COMPUTATIONAL LOGICS AND ARTIFICIAL INTELLIGENCE. . 2009
• Martín-mateos, Francisco Jesús, Rubio-garcia, Julio, Ruiz-Reina, Jose Luis:
  ACL2 VERIFICATION OF SIMPLICIAL DEGENERACY PROGRAMS IN THE KENZO SYSTEM. Comunicación en congreso. 16TH SYMPOSIUM ON THE INTEGRATION OF SYMBOLIC COMPUTATION AND MECHANISED REASONING. GRAND BEND, CÁNADA. 2009
• Martín-mateos, Francisco Jesús, Ruiz-Reina, Jose Luis, Rubio-García, Julio, Lambán-Pardo, Laureano:
  VERIFICACIÓN Y EFICIENCIA EN PROGRAMAS PARA EL CÁLCULO SIMBÓLICO: ESTUDIO DE UN CASO. Comunicación en congreso. IX JORNADAS SOBRE PROGRAMACIÓN Y LENGUAJES. SAN SEBASTIÁN. 2009
• Ruiz-Reina, Jose Luis, Greve-,David A., Kaufmann-,Matt, Manolios-,Panagiotis, Moore-,J Stroother, Ray-,Sandip, Vroon-,Daron, Sumners-,Rob, Wilding-,Matthew:
  EFFICIENT EXECUTION IN AN AUTOMATED REASONING ENVIRONMENT.. Comunicación en congreso. IX JORNADAS SOBRE PROGRAMACIÓN Y LENGUAJES. SAN SEBASTIÁN. 2009
• Hidalgo-Doblado, Maria Jose, Alonso-Jimenez, Jose Antonio, Martín-mateos, Francisco Jesús, Ruiz-Reina, Jose Luis:
  CONSTRUCTING FORMALLY VERIFIED REASONERS FOR THE ALC DESCRIPTION LOGIC. Comunicación en congreso. THIRD INTERNATIONAL WORKSHOP ON AUTOMATED SPECIFICATION AND VERIFICATION OF WEB SYSTEMS. VENECIA, ITALIA. 2007
• Alonso-Jimenez, Jose Antonio, Borrego-Diaz, Joaquin, Hidalgo-Doblado, Maria Jose, Martín-mateos, Francisco Jesús, Ruiz-Reina, Jose Luis:
  A FORMALLY VERIFIED PROVER FOR THE ALC DESCRIPTION LOGIC. Comunicación en congreso. THEOREM PROVING IN HIGHER ORDER LOGICS. KAISERSLAUTERN, ALEMANIA. 2007
• Martín-mateos, Francisco Jesús, Ruiz-Reina, Jose Luis, Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose:
  PROOF PEARL: A FORMAL PROOF OF HIGMAN'S LEMMA IN ACL2. Comunicación en congreso. THEOREM PROVING IN HIGHER ORDER LOGICS. OXFORD, REINO UNIDO. 2005
• Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Martín-mateos, Francisco Jesús, Ruiz-Reina, Jose Luis:
  A FORMALLY VERIFIED PROOF (IN PVS) OF THE STRONG COMPLETENESS THEOREM OF PROPOSITIONAL SLD-RESOLUTION. Comunicación en congreso. COMPUTER AIDED SYSTEMS THEORY. LAS PALMAS DE GRAN CANARIA, ESPAÑA. 2005
• Ruiz-Reina, Jose Luis:
  FORMAL VERIFICATION AND SYMBOLIC COMPUTATION SYSTEMS. Comunicación en congreso. EACA 2004 (9) (9.2004.SANTANDER, 1-3 JULIO). SANTANDER, 1-3 JULIO. 2004
• Ruiz-Reina, Jose Luis, Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Martín-mateos, Francisco Jesús:
  A FORMALLY VERIFIED QUADRATIC UNIFICATION ALGORITHM. Comunicación en congreso. FIFTH INTERNATIONAL WORKSHOP ON THE ACL2 THEOREM PROVER AND ITS APPLICATIONS. AUSTIN, TEXAS, USA. 2004
• Medina-Bulo, María Inmaculada, Palomo-Lozano, Francisco, Alonso-Jimenez, Jose Antonio, Ruiz-Reina, Jose Luis:
  VERIFIED COMPUTER ALGEBRA IN ACL2 (GRÖBNER BASIS COMPUTATION). Comunicación en congreso. 7TH INT. CONFERENCE ON ARTIFICIAL INTELLIGENCE AND SYMBOLIC COMPUTATION, AISC 2004 () (.2004.LINZ, AUSTRIA). LINZ, AUSTRIA. 2004
• Ruiz-Reina, Jose Luis, Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Martín-mateos, Francisco Jesús:
  FORMAL REASONING ABOUT EFFICIENT DATA STRUCTURES: A CASE STUDY IN ACL2. Comunicación en congreso. INTERNATIONAL WORKSHOP ON LOGIC BASED PROGRAM SYNTHESIS AND TRANSFORMATION. UPPSALA, SUECIA. 2003
• Martín-mateos, Francisco Jesús, Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Ruiz-Reina, Jose Luis:
  A FORMAL PROOF OF DICKSON'S LEMMA IN ACL2. Comunicación en congreso. INTERNATIONAL CONFERENCE ON LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE AND REASONING. ALMATY, KAZAKHSTAN. 2003
• Martín-mateos, Francisco Jesús, Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Ruiz-Reina, Jose Luis:
  FORMAL VERIFICATION OF MOLECULAR COMPUTATIONAL MODELS IN ACL2: A CASE STUDY. Comunicación en congreso. CONFERENCIA DE LA ASOCIACIÓN ESPAÑOLA PARA LA INTELIGENCIA ARTIFICIAL. SAN SEBASTIAN, ESPAÑA. 2003
• Ruiz-Reina, Jose Luis, Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Martín-mateos, Francisco Jesús:
  A THEORY ABOUT FIRST-ORDER TERMS IN ACL2. Comunicación en congreso. 3RD INTERNATIONAL WORKSHOP ON THE ACL2 THEOREM PROVER AND ITS APPLICATIONS. . 2002
• Martín-mateos, Francisco Jesús, Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Ruiz-Reina, Jose Luis:
  A GENERIC INSTANTIATION TOOL AND A CASE STUDY: A GENERIC MULTISET THEORY. Comunicación en congreso. 3RD INTERNATIONAL WORKSHOP ON THE ACL2 THEOREM PROVER AND ITS APPLICATIONS. . 2002
• Martín-mateos, Francisco Jesús, Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Ruiz-Reina, Jose Luis:
  VERIFICATION IN ACL2 OF A GENERIC FRAMEWORK TO SYNTHESIZE SAT-PROVERS. Comunicación en congreso. INTERNATIONAL WORKSHOP ON LOGIC BASED PROGRAM DEVELOPMENT AND TRANSFORMATION. . 2002
• Alonso-Jimenez, Jose Antonio, Borrego-Diaz, Joaquin, Hidalgo-Doblado, Maria Jose, Ruiz-Reina, Jose Luis:
  UNA INTRODUCCIÓN AL ANÁLISIS FORMAL DE CONCEPTOS EN PVS. Comunicación en congreso. I TALLER IBEROAMERICANO SOBRE DEDUCCION AUTOMATICA E INTELIGENCIA ARTIFICIAL. Santander (ESPAÑA). 2002
• Martín-mateos, Francisco Jesús, Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Ruiz-Reina, Jose Luis:
  DESARROLLO FORMAL Y VERIFICACIÓN DE SISTEMAS PROPOSICIONALES. Comunicación en congreso. I TALLER IBEROAMERICANO SOBRE DEDUCCION AUTOMATICA E INTELIGENCIA ARTIFICIAL. Santander (ESPAÑA). 2002
• Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Ruiz-Reina, Jose Luis:
  DESARROLLO FORMAL Y VERIFICACIÓN DE SISTEMAS PROPOSICIONALES. Comunicación en congreso. I TALLER IBEROAMERICANO SOBRE DEDUCCION AUTOMATICA E INTELIGENCIA ARTIFICIAL. Santander (ESPAÑA). 2002
• Alonso-Jimenez, Jose Antonio, Borrego-Diaz, Joaquin, Hidalgo-Doblado, Maria Jose, Martín-mateos, Francisco Jesús, Ruiz-Reina, Jose Luis:
  UNA INTRODUCCIÓN AL ANÁLISIS FORMAL DE CONCEPTOS EN PVS. Comunicación en congreso. I TALLER IBEROAMERICANO SOBRE DEDUCCION AUTOMATICA E INTELIGENCIA ARTIFICIAL. Santander (ESPAÑA). 2002
• Ruiz-Reina, Jose Luis, Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Martín-mateos, Francisco Jesús:
  VERIFICACIÓN FORMAL Y EFICIENCIA: UN CASO DE ESTUDIO APLICADO A LA UNIFICACIÓN DE TÉRMINOS. Comunicación en congreso. I TALLER IBEROAMERICANO SOBRE DEDUCCION AUTOMATICA E INTELIGENCIA ARTIFICIAL. Santander (ESPAÑA). 2002
• Ruiz-Reina, Jose Luis, Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Martín-mateos, Francisco Jesús:
  PROGRESS REPORT: TERM DAGS USING STOBJS. Comunicación en congreso. 3RD INTERNATIONAL WORKSHOP ON THE ACL2 THEOREM PROVER AND ITS APPLICATIONS. . 2002
• Martín-mateos, Francisco Jesús, Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Ruiz-Reina, Jose Luis:
  VERIFYING AN APPLICATIVE ATP USING MULTISET RELATIONS. Comunicación en congreso. 7TH INTERNATIONAL CONFERENCE ON COMPUTER AIDED SYSTEMS THEORY. LAS PALMAS DE GRAN CANARIA. 2001
• Ruiz-Reina, Jose Luis, Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Martín-mateos, Francisco Jesús:
  MULTISET RELATIONS: A TOOL FOR PROVING TERMINATION. Comunicación en congreso. 2ND ACL2 WORKSHOP. AUSTIN, TEXAS, EEUU. 2000
• Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Martín-mateos, Francisco Jesús, Ruiz-Reina, Jose Luis:
  FORMALIZACIÓN DEL RAZONAMIENTO ECUACIONAL EN UNA LÓGICA COMPUTACIONAL. Comunicación en congreso. ENCUENTRO DE MATEMÁTICOS ANDALUCES. Santander (ESPAÑA). 2000
• Ruiz-Reina, Jose Luis, Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Martín-mateos, Francisco Jesús:
  FORMALIZING REWRITING IN THE ACL2 THEOREM PROVER. Comunicación en congreso. 5TH INTERNATIONAL CONFERENCE ON ARTIFICIAL INTELLIGENCE AND SYMBOLIC COMPUTATION. . 2000
• Ruiz-Reina, Jose Luis, Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Martín-mateos, Francisco Jesús:
  A MECHANICAL PROOF OF KNUTH-BENDIX CRITICAL PAIR THEOREM (USING ACL2). Comunicación en congreso. 3RD FIRST-ORDER THEOREM PROVING. ST ANDREWS, SCOTLAND. 2000
• Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Ruiz-Reina, Jose Luis:
  FORMALIZACIÓN DEL RAZONAMIENTO ECUACIONAL EN UNA LÓGICA COMPUTACIONAL. Comunicación en congreso. ENCUENTRO DE MATEMÁTICOS ANDALUCES. Santander (ESPAÑA). 2000
• Ruiz-Reina, Jose Luis, Martín-mateos, Francisco Jesús, Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose:
  MECHANICAL VERIFICATION OF A RULE-BASED UNIFICATION ALGORITHM IN THE BOYER-MOORE THEOREM PROVER. Comunicación en congreso. JOINT CONFERENCE ON DECLARATIVE PROGRAMMING. L'AQUILA, ITALIA. 1999
• Ruiz-Reina, Jose Luis, Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Martín-mateos, Francisco Jesús:
  VERIFICACIÓN AUTOMÁTICA DE SISTEMAS DE RAZONAMIENTO (APLICACIÓN A LA ENSEÑANZA DE LA INTELIGENCIA ARTIFICIAL). Comunicación en congreso. IV JORNADAS SOBRE LA ENSEÑANZA UNIVERSITARIA DE LA INFORMATICA. ANDORRA. 1998
• Martín-mateos, Francisco Jesús, Alonso-Jimenez, Jose Antonio, Hidalgo-Doblado, Maria Jose, Ruiz-Reina, Jose Luis:
  RAZONAMIENTO AUTOMÁTICO EN SISTEMAS DE REPRESENTACIÓN DEL CONOCIMIENTO (Y SU RELACIÓN CON LA ENSEÑANZA DE LA INTELIGENCIA ARTIFICIAL). Comunicación en congreso. IV JORNADAS SOBRE LA ENSEÑANZA UNIVERSITARIA DE LA INFORMATICA. ANDORRA. 1998
• Arrabal-Parrilla, Juan Jose, Balbontin-Noval, Delia, Alonso-Jimenez, Jose Antonio, Lara-Martin, Francisco Felix, Martín-mateos, Francisco Jesús, Pérez-Jiménez, Mario Jesús, Ruiz-Reina, Jose Luis:
  GTI: UNA HERRAMIENTA DE EDICIÓN DE CURSOS ADAPTATIVOS. Comunicación en congreso. XIII CONGRESO NACIONAL DE INGENIERÍA DE PROYECTOS. Santander (ESPAÑA). 1997
• Ruiz-Reina, Jose Luis, Gegúndez-Arias, Manuel Emilio:
  PRUEBA POR CONSISTENCIA DE TEOREMAS INDUCTIVOS: INDUCCION SIN INDUCCION. Comunicación en congreso. CONGRESO DE LENGUAJES NATURALES Y LENGUAJES FORMALES (10.1994.SEVILLA). . 1994

Tesis dirigidas y co-dirigidas:

• Medina-Bulo, María Inmaculada:
  VERIFICACIÓN FORMAL EN ACL2 DEL ALGORITMO DE BUCHBERGER. Tesis Doctoral. 2003