Francisco Jesús Martín Mateos
Telefono: 95.455.78.83
Email: Solicitar correo
Perfil en ORCID: 0000-0002-9795-1683
Perfil en Scopus: 6602636680
Perfil en Dialnet: 2653851

Grupo de Investigación: Logica, Computacion e Ingenieria del Conocimiento
Departamento/Unidad: Ciencias de la Computación e Inteligencia Artificial
Situación profesional: Profesor Titular de Universidad

Responsable de los siguientes proyectos/ayudas en la US:

• Contrato con empresas (Arts. 68/83 LOU):
  • Informe técnico sobre aplicabilidad de Sistemas Basados en el Conocimiento al proyecto SOLEME (P025-11/E19)
  
  

Participa en los siguientes proyectos/ayudas en la US:

• Proyecto de investigación:
  • Lógica Computacional para la Ciencia del Dato (TIN2013-41086-P - Equipo de Investigación)
  • Gestión mecanizada del conocimiento matemático. Aplicaciones en lógica (MTM2009-13842-C02-02 - Investigador)
  • Sistemas verificados para razonamiento en la Web semántica (TIN2004-03884 - Investigador)
  • Desarrollo y verificación formal de sistemas de razonamiento (TIC2000-1368-C03-02 - Investigador)
  
  
• Ayuda a la investigación:
  • Incentivo al Grupo de Investigación TIC-137 (2017/TIC-137 - Investigador)
  • Ayuda a la Consolidación del Grupo de Investigación TIC-137 (2007/TIC-137 - Investigador)
  • Ayuda a la Consolidación del Grupo de Investigación TIC-137 (2006/TIC-137 - Investigador)
  • Ayuda a la Consolidación del Grupo de Investigación TIC-137 (2005/TIC-137 - Investigador)
  
  

Cobertura de la base de datos de proyectos, véase aqui

Publicaciones:

Libros

Alonso Jimenez, Jose Antonio, Aranda Corral, Gonzalo A., Chavez Gonzalez, Antonia Mª, Cordon Franco, Andres, Hidalgo Doblado, Maria Jose, et. al.:
Exámenes de Programación funcional con Haskell (2009-2015). OpenLibra. 2015. 602

Otra participación en Libros

Quesada Moreno, Jose Francisco (Editor/a), Martín Mateos, Francisco Jesús (Editor/a):
Future and Emerging Trends in Language Technology. Machine Learning and Big Data. 2017

Quesada Moreno, Jose Francisco (Editor/a), Martín Mateos, Francisco Jesús (Editor/a), Lopez Soto, Teresa (Editor/a):
Future and Emerging Trends in Language Technology. Machine Learning and Big Data. Berlin Springer Verlag. 2017

Quesada Moreno, Jose Francisco (Editor/a), Martín Mateos, Francisco Jesús (Editor/a), Lopez Soto, Teresa (Editor/a):
Future and Emergent Trends in Language Technology. Swizerland. Springer. 2016. 160. ISBN 9783319334998

Capítulos en Libros

Serrano Bello, Rafael, González Valencia, Luis Carlos, Martín Mateos, Francisco Jesús:
Sensorización y Control de un Proceso de Mecanizado Utilizando un Sistema Experto Basado en Reglas. Pag. 2088-2100. En: Actas del XIV Congreso Internacional de Ingeniería de Proyectos. Asociacion Española de Ingeniería de Proyectos. 2010. ISBN 978-84-614-2607-2

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. Logroño, España. Universidad de la Rioja. 2010. ISBN 978-84-96487-50-5

Martín Mateos, Francisco Jesús, González Valencia, Luis Carlos, Serrano Bello, Rafael:
Sistema Experto para el Control en Tiempo Real de Procesos de Mecanizado. Pag. 477-496. En: Actas de la XIII Conferencia de la Asociación Española para la Inteligencia Artificial. Santander (ESPAÑA). Asociación Española para la Inteligencia Artificial. 2009. ISBN 978-84-692-6424-9

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. San Sebastián, España. 2009. ISBN 978-84-692-4600-9

Alonso Jimenez, Jose Antonio, Aranda Corral, Gonzalo A., Martín Mateos, Francisco Jesús:
Krrt: Knowledge Representation and Reasoning Tutor System. Pag. 150-151. En: Computer Aided Systems Theory. Las Palmas de Gran Canaria, España. Iuctc Universidad de las Palmas de Gran Canaria. 2007. ISBN 978-84-690-3603-7

Martín Mateos, Francisco Jesús:
Sistema Experto para la Simulación de Sistemas Tácticos de Baloncesto con Software Libre. Pag. 38-51. En: Proceedings of the Floss International Conference 2007. Cadiz, España. Servicio de Publicaciones de la Universidad de Cádiz. 2007. ISBN 978-84-9828-124-8

Alonso Jimenez, Jose Antonio, Aranda Corral, Gonzalo A., Martín Mateos, Francisco Jesús:
Fits: Formalization With an Intelligent Tutor System. Vol. 2. Pag. 861-865. En: Current Developments in Technology-Assisted Education (2006). Badajoz, España. Formatex. 2006. ISBN 84-690-2472-8

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. Vol. I. Pag. 235-244. En: CAEPIA-TTIA 2003. San Sebastián. Universidad del País Vasco. 2003. ISBN 84-8373-564-4

Ruiz Reina, Jose Luis, Alonso Jimenez, Jose Antonio, Hidalgo Doblado, Maria Jose, Martín Mateos, Francisco Jesús:
Termination in Acl2 Using Multiset Relation. Vol. 28. Pag. 217-245. En: Thirty Five Years of Automating Mathematics. Dordrecht, Holanda. Kluwer Academic Publishers. 2003. ISBN 1-4020-1656-5

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. Vol. II. 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, 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). . Barcelona, España. Enginyeria I Arquitectura la Salle. 1998. ISBN 84-922538-3-5

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). . Barcelona, España. 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, et. al.:
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

Publicaciones en Revistas

Heras, Jónathan, Martín Mateos, Francisco Jesús, Pascual, Vico:
Modelling Algebraic Structures and Morphisms in ACL2. En: Applicable Algebra in Engineering, Communications and Computing. 2015. Vol. 26. Núm. 3. Pag. 277-303. 10.1007/s00200-015-0252-9

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

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. 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

Martín Mateos, Francisco Jesús, González Valencia, Luis Carlos, Serrano Bello, Rafael:
Expert System to Real Time Control of Machining Processes. En: Lecture Notes in Computer Science. 2010. Vol. 5988. Pag. 281-290. 10.1007/978-3-642-14264-2_29

Serrano Bello, Rafael, González Valencia, Luis Carlos, Martín Mateos, Francisco Jesús:
Architecture for the Optimization of a Machining Process in Real Time Through Rule-Based Expert System. En: AIP Conference Proceedings. 2009. Vol. 1181. Pag. 652-661

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. Pag. 106-121

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. Pag. 135-150

Alonso Jimenez, Jose Antonio, Aranda Corral, Gonzalo Antonio, Martin Mateos, Francisco Jesus:
Krrt: Knowledge Representation and Reasoning Tutor System. En: Lecture Notes in Computer Science. 2007. Vol. 4739. Pag. 400-407

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

Alonso Jimenez, Jose Antonio, Borrego Diaz, Joaquin, Chavez Gonzalez, Antonia Mª, Martin Mateos, Francisco Jesus:
Foundational Challenges in Automated Semantic Web Data and Ontology Cleaning. En: IEEE Intelligent Systems and Their Applications. 2006. Vol. 21. Núm. 1. Pag. 42-52

Palomo Duarte, Manuel, Martin Mateos, Francisco Jesus, Alonso Jimenez, Jose Antonio:
Rete Algorithm Applied to Robotic Soccer. En: Lecture Notes in Computer Science. 2005. Vol. 3643. Pag. 571-576

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. 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

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. 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. Pag. 344-353

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. Pag. 182-198

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. Pag. 49-58

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

Graciani Díaz, Mª del Carmen, Martin Mateos, Francisco Jesus, Pérez Jiménez, Mario Jesús:
Specification of Adleman's Restricted Model Using an Automated Reasoning System: Verification of Lipton's Experiment. En: Lecture Notes in Computer Science. 2002. Vol. 2509. Pag. 126-136

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. 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. Pag. 612-626

Martín Mateos, Francisco Jesús:
Razonamiento Automático en Lógicas Polivalentes Mediante Métodos Algebraicos en Maple. En: TQ (Albacete). 1996. Vol. 3. Pag. 52-70

Otra participación en Libros de Actas

Martín Mateos, Francisco Jesús (Editor/a):
12th International Conference on Artificial Intelligence and Symbolic Computation AISC 2014. 2014. ISBN 978-3-319-13769-8

Martín Mateos, Francisco Jesús (Editor/a):
Computational Logics and Artificial Intelligence. 2009. 131. 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

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

Heras, Jonathan, Martín Mateos, Francisco Jesús, Pascual, Vico:
An Acl2 Formalization of Algebraic Structures. Comunicación en congreso. XIII Encuentro de Álgebra Computacional y Aplicaciones. Alcalá de Henares. 2012

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

González Valencia, Luis Carlos, Serrano Bello, Rafael, Martín Mateos, Francisco Jesús:
Sensorización y Control de un Proceso de Mecanizado Utilizando un Sistema Experto Basado en Reglas. Comunicación en congreso. International Congress on Project Engineering. 2010

González Valencia, Luis Carlos, Serrano Bello, Rafael, Martín Mateos, Francisco Jesús:
Expert System for Machining Process Control. Comunicación en congreso. Rapid Product Developement Event. Marinha Grande, Açores, Portugal. 2010

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:
Sistema Experto para el Control en Tiempo Real de Procesos de Mecanizado. Conferencia en Jornada no publicada. II Jornadas de Lógica, Computación e Inteligencia Artificial. Santander (ESPAÑA). 2009

Serrano Bello, Rafael, González Valencia, Luis Carlos, Martín Mateos, Francisco Jesús:
Arquitectura para la Optimización de un Proceso de Mecanizado en Tiempo Real Mediante un Sistema Experto. Comunicación en congreso. Third Manufacturing Engineering Society International Conference. Alcoy, Valencia. 2009. Third Manufacturing Engineering Society International Conference. 378. 341

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. Intelligent Computer Mathematics. 106. 121

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. IX Jornadas Sobre Programación y Lenguajes. 7. 14

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. Computational Logics and Artificial Intelligence. 35. 45

Martín Mateos, Francisco Jesús, González Valencia, Luis Carlos, Serrano Bello, Rafael:
Sistema Experto para el Control en Tiempo Real de Procesos de Mecanizado. Comunicación en congreso. Conferencia de la Asociación Española para la Inteligencia Artificial. Santander (ESPAÑA). 2009. Actas de la XIII Conferencia de la Asociación Española para la Inteligencia Artificial. 477. 486

Palomo Duarte, Manuel, Martín Mateos, Francisco Jesús:
Sistema Experto para la Simulación de Sistemas Tácticos de Baloncesto con Software Libre. Comunicación en congreso. Free/Libre/Open Source Systems International Conference. Cádiz. 2007

Martín Mateos, Francisco Jesús:
El Sistema de Razonamiento Automático Otter. Conferencia en Jornada no publicada. Jornadas de Ingeniería y Tecnologías Informáticas. Cádiz. 2007

Alonso Jimenez, Jose Antonio, Aranda Corral, Gonzalo A., Martín Mateos, Francisco Jesús:
Krrt: Knowledge Representation & Reasoning Tutor System. Comunicación en congreso. International Conference on Computer Aided Systems Theory. Las Palmas de Gran Canaria, Spain. 2007. Computer Aided Systems Theory - Eurocast 2007. 280. 283

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. Proceedings of the 3rd International Workshop on Automated Specification and Verification of Web Systems. 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. Comunicación en congreso. Theorem Proving in Higher Order Logics. Kaiserslautern, Alemania. 2007. Theorem Proving in Higher Order Logics. 135. 150

Martín Mateos, Francisco Jesús:
Verified Computer Algebra in a Computational Logic. Conferencia Congreso no publicada. Mathematics, Algorithms and Proofs. Castro Urdiales, España. 2006

Alonso Jimenez, Jose Antonio, Aranda Corral, Gonzalo A., Martín Mateos, Francisco Jesús:
Fits: Formalization With an Intelligent Tutor System. Comunicación en congreso. IV International Conference on Multimedia and Information and Communication Technologies in Education. Santander (ESPAÑA). 2006

Palomo Duarte, Manuel, Martín Mateos, Francisco Jesús, Alonso Jimenez, Jose Antonio:
Rete Algorithm Applied to Robotic Soccer. Comunicación en congreso. Computer Aided Systems Theory. Las Palmas de Gran Canaria, España. 2005. Cast and Tools for Robotics, Vehicular and Communication Systems. 280. 283

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. Cast and Tools for Robotics, Vehicular and Communication Systems. 83. 86

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. Theorem Proving in Higher Order Logics. 358. 372

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

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. LOPSTR 2003, Preproceedings of the International Symposium of Logic Based Program Synthesis and Transformation. 97. 112

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. Proceedings of the International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2003. 49. 58

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. X Conferencia de la Asocicación Española para la Inteligencia Artificial. 235. 240

Martín Mateos, Francisco Jesús, Alonso Jimenez, Jose Antonio, Pérez Jiménez, Mario Jesús, Sancho Caparrini, Fernando:
Molecular Computation Models in Acl2: a Simulation of Lipton's Experiment Solving SAT. 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:
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

Graciani Díaz, Mª del Carmen, Martín Mateos, Francisco Jesús, Pérez Jiménez, Mario Jesús:
Specification of Adleman`s Restricted Model Using an Automated Reasoning System: Verification of Lipton`s Experiment. Comunicación en congreso. 3rd International Conference on Unconventional Models of Computation. Kobe, Japón. 2002. Unconventional Models of Computation. 126. 136

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. 3RD International Conference on Pain and Physiotherapy. 78. 100

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. 3rd International Workshop on the Acl2 Theorem Prover and Its Applications. 101. 108

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. 3RD International Conference on Pain and Physiotherapy. 188. 203

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. I Taller Iberoamericano Sobre Deduccion Automatica e Inteligencia Artificial. 77. 90

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. Preproceedings of the International Workshop on Logic Based Program Development and Transformation. 182. 197

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. Eurocast 2001 Conference. 612. 626

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. Proceedings of the Acl2 Workshop 2000. 82. 91

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. Proceedings of the Third International Workshop on First-Order Theorem Proving. 206. 216

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. Artificial Intelligence and Symbolic Computation, Aisc 2000, Revised Papers. 92. 106

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. Actas del Encuentro de Matemáticos Andaluces. 41. 50

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. Proc. of Joint Conference on Declarative Programming. 289. 304

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. IV Jornades Sobre L'ensenyament Universitari de la Infomàtica. 297. 304

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. IV Jornades Sobre L'ensenyament Universitari de la Infomàtica. 289. 296

Arrabal Parrilla, Juan Jose, Balbontin Noval, Delia, Alonso Jimenez, Jose Antonio, Lara Martin, Francisco Felix, Martín Mateos, Francisco Jesús, et. al.:
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. Actas del XIII Congreso Nacional de Ingenieria de Proyectos. 627. 634

Martín Mateos, Francisco Jesús:
Razonamiento Automático en Lógicas Polivalentes Mediante Métodos Algebraicos en Maple. Comunicación en congreso. II Congreso de Usuarios de Maple V. Santander (ESPAÑA). 1996. Actas del II Congreso de Usuarios de Maple. 52. 70

Tesis dirigidas y co-dirigidas:

Serrano Suarez, Fabián Fernando:
Formalización en Isar de la Metalógica de Primer Orden. Tesis Doctoral. 2012