Directorio
FRANCISCO JESUS MARTIN MATEOS
Categoría
Profesor Titular de Universidad
Departamento
Área
Ciencia de la Computación e Inteligenc. Artificial
Docencia
Investigación
Grupo de investigación
LOGICA, COMPUTACION E INGENIERIA DEL CONOCIMIENTO (LOCIC)
Proyectos y contratos de investigación
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)
SISTEMAS VERIFICADOS PARA RAZONAMIENTO EN LA WEB SEMÁNTICA (TIN2004-03884 - Investigador/a)
GESTIÓN MECANIZADA DEL CONOCIMIENTO MATEMÁTICO. APLICACIONES EN LÓGICA (MTM2009-13842-C02-02 - Investigador/a)
INVESTIGACIÓN DE LOS FACTORES CRÍTICOS DE LOS PROCESOS DE FABRICACIÓN BÁSICOS DEL SECTOR AERONÁUTICO ANDALUZ, SENSOR-IA (FIDETIA P044-07/E19 - Responsable)
REALIZACIÓN DEL ESTUDIO DEL ARTE PARA EL PROYECTO EVAPREX (FIDETIA P029-08/E19 - Responsable)
Informe técnico sobre aplicabilidad de Sistemas Basados en el Conocimiento al proyecto SOLEME (P025-11/E19 - Responsable)
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)
SISTEMAS DE ENSEÑANZA ASISTIDA POR ORDENADOR EN EL PROYECTO ATLAS (CICYT 95-0350 - Investigador/a)
INFORME TÉCNICO SOBRE APLICABILIDAD DE SISTEMAS BASADOS EN EL CONOCIMIENTO AL PROYECTO SOLEME (FIDETIA P025-11/E19 - Responsable)
GESTIÓN MECANIZADA DEL CONOCIMIENTO MATEMÁTICO. LOS CASOS DE LA TOPOLOGÍA ALGEBRAICA Y LA LÓGICA (MTM2009-13842-C02-01 - Investigador/a)
Libros publicados
Quesada-Moreno, Jose Francisco;Martín-mateos, Francisco Jesús;Lopez-Soto, Teresa:
Future and Emerging Trends in Language Technology. Machine Learning and Big Data. Berlin Springer Verlag. 2017.
Future and Emerging Trends in Language Technology. Machine Learning and Big Data. Berlin Springer Verlag. 2017.
Quesada-Moreno, Jose Francisco;Martín-mateos, Francisco Jesús;Lopez-Soto, Teresa:
Future and Emergent Trends in Language Technology. Springer. 2016. 9783319334998
Future and Emergent Trends in Language Technology. Springer. 2016. 9783319334998
Alonso-Jimenez, Jose Antonio;Riscos-Nuñez, Agustin;Valencia-Cabrera, Luis;Aranda-Corral, Gonzalo A.;Chavez-Gonzalez, Antonia Mª;Cordon-Franco, Andres;Hidalgo-Doblado, Maria Jose;Martín-mateos, Francisco Jesús;Martínez-del-Amor, Miguel Ángel;Pérez-Hurtado De Mendoza, Ignacio;Quesada-Moreno, Jose Francisco:
Exámenes de Programación funcional con Haskell (2009-2015). OpenLibra. 2015.
Exámenes de Programación funcional con Haskell (2009-2015). OpenLibra. 2015.
Capítulos en Libros
Lambán-Pardo, Laureano;Martín-mateos, Francisco Jesús;Ruiz-Reina, Jose Luis:
TOPOLOGÍA SIMPLICIAL EN ACL2. Pág. 1-20. UNIVERSIDAD DE LA RIOJA. UNIVERSIDAD DE LA RIOJA. 2010.
TOPOLOGÍA SIMPLICIAL EN ACL2. Pág. 1-20. UNIVERSIDAD DE LA RIOJA. UNIVERSIDAD DE LA RIOJA. 2010.
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. Pág. 2088-2100. ASOCIACION ESPAÑOLA DE INGENIERÍA DE PROYECTOS. ASOCIACION ESPAÑOLA DE INGENIERÍA DE PROYECTOS. 2010.
SENSORIZACIÓN Y CONTROL DE UN PROCESO DE MECANIZADO UTILIZANDO UN SISTEMA EXPERTO BASADO EN REGLAS. Pág. 2088-2100. ASOCIACION ESPAÑOLA DE INGENIERÍA DE PROYECTOS. ASOCIACION ESPAÑOLA DE INGENIERÍA DE PROYECTOS. 2010.
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. Pág. 477-496. ASOCIACIÓN ESPAÑOLA PARA LA INTELIGENCIA ARTIFICIAL. ASOCIACIÓN ESPAÑOLA PARA LA INTELIGENCIA ARTIFICIAL. 2009.
SISTEMA EXPERTO PARA EL CONTROL EN TIEMPO REAL DE PROCESOS DE MECANIZADO. Pág. 477-496. ASOCIACIÓN ESPAÑOLA PARA LA INTELIGENCIA ARTIFICIAL. ASOCIACIÓN ESPAÑOLA PARA LA INTELIGENCIA ARTIFICIAL. 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. Pág. 7-14. 2009.
VERIFICACIÓN Y EFICIENCIA EN PROGRAMAS PARA EL CÁLCULO SIMBÓLICO: ESTUDIO DE UN CASO. Pág. 7-14. 2009.
Martín-mateos, Francisco Jesús:
SISTEMA EXPERTO PARA LA SIMULACIÓN DE SISTEMAS TÁCTICOS DE BALONCESTO CON SOFTWARE LIBRE. Pág. 38-51. SERVICIO DE PUBLICACIONES DE LA UNIVERSIDAD DE CÁDIZ. SERVICIO DE PUBLICACIONES DE LA UNIVERSIDAD DE CÁDIZ. 2007.
SISTEMA EXPERTO PARA LA SIMULACIÓN DE SISTEMAS TÁCTICOS DE BALONCESTO CON SOFTWARE LIBRE. Pág. 38-51. SERVICIO DE PUBLICACIONES DE LA UNIVERSIDAD DE CÁDIZ. SERVICIO DE PUBLICACIONES DE LA UNIVERSIDAD DE CÁDIZ. 2007.
Alonso-Jimenez, Jose Antonio;Aranda-Corral, Gonzalo A.;Martín-mateos, Francisco Jesús:
KRRT: KNOWLEDGE REPRESENTATION AND REASONING TUTOR SYSTEM. Pág. 150-151. IUCTC UNIVERSIDAD DE LAS PALMAS DE GRAN CANARIA. IUCTC UNIVERSIDAD DE LAS PALMAS DE GRAN CANARIA. 2007.
KRRT: KNOWLEDGE REPRESENTATION AND REASONING TUTOR SYSTEM. Pág. 150-151. IUCTC UNIVERSIDAD DE LAS PALMAS DE GRAN CANARIA. IUCTC UNIVERSIDAD DE LAS PALMAS DE GRAN CANARIA. 2007.
Alonso-Jimenez, Jose Antonio;Aranda-Corral, Gonzalo A.;Martín-mateos, Francisco Jesús:
FITS: FORMALIZATION WITH AN INTELLIGENT TUTOR SYSTEM. Pág. 861-865. En: 2. FORMATEX. FORMATEX. 2006.
FITS: FORMALIZATION WITH AN INTELLIGENT TUTOR SYSTEM. Pág. 861-865. En: 2. FORMATEX. FORMATEX. 2006.
Ruiz-Reina, Jose Luis;Alonso-Jimenez, Jose Antonio;Hidalgo-Doblado, Maria Jose;Martín-mateos, Francisco Jesús:
TERMINATION IN ACL2 USING MULTISET RELATION. Pág. 217-245. En: 28. KLUWER ACADEMIC PUBLISHERS. KLUWER ACADEMIC PUBLISHERS. 2003.
TERMINATION IN ACL2 USING MULTISET RELATION. Pág. 217-245. En: 28. KLUWER ACADEMIC PUBLISHERS. KLUWER ACADEMIC PUBLISHERS. 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. Pág. 235-244. En: I. UNIVERSIDAD DEL PAÍS VASCO. UNIVERSIDAD DEL PAÍS VASCO. 2003.
FORMAL VERIFICATION OF MOLECULAR COMPUTATIONAL MODELS IN ACL2: A CASE STUDY. Pág. 235-244. En: I. UNIVERSIDAD DEL PAÍS VASCO. UNIVERSIDAD DEL PAÍS VASCO. 2003.
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. Pág. 41-50. En: II. SECRETARIADO DE PUBLICACIONES - UNIVERSIDAD DE SEVILLA. SECRETARIADO DE PUBLICACIONES - UNIVERSIDAD DE SEVILLA. 2001.
FORMALIZACIÓN DEL RAZONAMIENTO ECUACIONAL EN UNA LÓGICA COMPUTACIONAL. Pág. 41-50. En: II. SECRETARIADO DE PUBLICACIONES - UNIVERSIDAD DE SEVILLA. SECRETARIADO DE PUBLICACIONES - UNIVERSIDAD DE SEVILLA. 2001.
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). Pág. 297-304. ENGINYERIA I ARQUITECTURA LA SALLE. ENGINYERIA I ARQUITECTURA LA SALLE. 1998.
VERIFICACIÓN AUTOMÁTICA DE SISTEMAS DE RAZONAMIENTO (APLICACIÓN A LA ENSEÑANZA DE LA INTELIGENCIA ARTIFICIAL). Pág. 297-304. ENGINYERIA I ARQUITECTURA LA SALLE. ENGINYERIA I ARQUITECTURA LA SALLE. 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). Pág. 289-296. ENGINYERIA I ARQUITECTURA LA SALLE. ENGINYERIA I ARQUITECTURA LA SALLE. 1998.
RAZONAMIENTO AUTOMÁTICO EN SISTEMAS DE REPRESENTACIÓN DEL CONOCIMIENTO (Y SU RELACIÓN CON LA ENSEÑANZA DE LA INTELIGENCIA ARTIFICIAL). Pág. 289-296. ENGINYERIA I ARQUITECTURA LA SALLE. ENGINYERIA I ARQUITECTURA LA SALLE. 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. Pág. 627-634. ANTONIO F. MARTIN NAVARRO. ANTONIO F. MARTIN NAVARRO. 1997.
GTI: UNA HERRAMIENTA DE EDICIÓN DE CURSOS ADAPTATIVOS. Pág. 627-634. ANTONIO F. MARTIN NAVARRO. ANTONIO F. MARTIN NAVARRO. 1997.
Participación en congresos
Martín-mateos, Francisco Jesús:
12th International Conference on Artificial Intelligence and Symbolic Computation AISC 2014. Escuela Técnica Superior de Ingeniería Informática de la Universidad de Sevilla. 2014
12th International Conference on Artificial Intelligence and Symbolic Computation AISC 2014. Escuela Técnica Superior de Ingeniería Informática de la Universidad de Sevilla. 2014
Asistencia 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
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
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
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
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
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
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:
EXPERT SYSTEM FOR MACHINING PROCESS CONTROL. Comunicación en congreso. RAPID PRODUCT DEVELOPEMENT EVENT. MARINHA GRANDE, AÇORES, PORTUGAL. 2010
EXPERT SYSTEM FOR MACHINING PROCESS CONTROL. Comunicación en congreso. RAPID PRODUCT DEVELOPEMENT EVENT. MARINHA GRANDE, AÇORES, PORTUGAL. 2010
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
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
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
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
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;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
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
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
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
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
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
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
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
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
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
A FORMALLY VERIFIED PROVER FOR THE ALC DESCRIPTION LOGIC. Comunicación en congreso. THEOREM PROVING IN HIGHER ORDER LOGICS. KAISERSLAUTERN, ALEMANIA. 2007
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
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
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
KRRT: KNOWLEDGE REPRESENTATION & REASONING TUTOR SYSTEM. Comunicación en congreso. INTERNATIONAL CONFERENCE ON COMPUTER AIDED SYSTEMS THEORY. LAS PALMAS DE GRAN CANARIA, SPAIN. 2007
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
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
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
VERIFIED COMPUTER ALGEBRA IN A COMPUTATIONAL LOGIC. Conferencia Congreso no publicada. MATHEMATICS, ALGORITHMS AND PROOFS. CASTRO URDIALES, ESPAÑA. 2006
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
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
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
RETE ALGORITHM APPLIED TO ROBOTIC SOCCER. Comunicación en congreso. COMPUTER AIDED SYSTEMS THEORY. LAS PALMAS DE GRAN CANARIA, ESPAÑA. 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
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;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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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;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
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
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
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
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
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
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:
MULTISET RELATIONS: A TOOL FOR PROVING TERMINATION. Comunicación en congreso. 2ND ACL2 WORKSHOP. AUSTIN, TEXAS, EEUU. 2000
MULTISET RELATIONS: A TOOL FOR PROVING TERMINATION. Comunicación en congreso. 2ND ACL2 WORKSHOP. AUSTIN, TEXAS, EEUU. 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
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
A MECHANICAL PROOF OF KNUTH-BENDIX CRITICAL PAIR THEOREM (USING ACL2). Comunicación en congreso. 3RD FIRST-ORDER THEOREM PROVING. ST ANDREWS, SCOTLAND. 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
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
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
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
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
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
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
Artículos publicados
Heras, Jónathan;Martín-mateos, Francisco Jesús;Pascual, Vico:
Modelling Algebraic Structures and Morphisms in ACL2. Applicable Algebra in Engineering, Communications and Computing. 2015. Vol: 26. Núm: 3. Pág. 277-303. 10.1007/s00200-015-0252-9.
Modelling Algebraic Structures and Morphisms in ACL2. Applicable Algebra in Engineering, Communications and Computing. 2015. Vol: 26. Núm: 3. Pág. 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. Journal of Automated Reasoning. 2014. Vol: 52. Núm: 3. Pág. 331-360. 10.1007/s10817-013-9291-8.
FORMALLY VERIFIED TABLEAU-BASED REASONERS FOR A DESCRIPTION LOGIC. Journal of Automated Reasoning. 2014. Vol: 52. Núm: 3. Pág. 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. Interest Group in Pure and Applied Logics. Logic Journal. 2014. Vol: 22. Núm: 1. Pág. 39-65. 10.1093/jigpal/jzt034.
VERIFYING THE BRIDGE BETWEEN SIMPLICIAL TOPOLOGY AND ALGEBRA: THE EILENBERG¿ZILBER ALGORITHM. Interest Group in Pure and Applied Logics. Logic Journal. 2014. Vol: 22. Núm: 1. Pág. 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. Annals of Mathematics and Artificial Intelligence. 2012. Vol: 64. Núm: 1. Pág. 1-37. 10.1007/s10472-011-9274-6.
FORMALIZATION OF A NORMALIZATION THEOREM IN SIMPLICIAL TOPOLOGY. Annals of Mathematics and Artificial Intelligence. 2012. Vol: 64. Núm: 1. Pág. 1-37. 10.1007/s10472-011-9274-6.
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. Journal of Automated Reasoning. 2011. Vol: 47. Núm: 3. Pág. 229-250. 10.1007/s10817-010-9178-x.
PROOF PEARL: A FORMAL PROOF OF HIGMAN'S LEMMA IN ACL2. Journal of Automated Reasoning. 2011. Vol: 47. Núm: 3. Pág. 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. Lecture Notes in Computer Science. 2011. Vol: 6898. Pág. 200-215.
APPLYING ACL2 TO THE FORMALIZATION OF ALGEBRAIC TOPOLOGY: SIMPLICIAL POLYNOMIALS. Lecture Notes in Computer Science. 2011. Vol: 6898. Pág. 200-215.
Martín-mateos, Francisco Jesús;González-Valencia, Luis Carlos;Serrano-Bello, Rafael:
EXPERT SYSTEM TO REAL TIME CONTROL OF MACHINING PROCESSES. Lecture Notes in Computer Science. 2010. Vol: 5988. Pág. 281-290. 10.1007/978-3-642-14264-2_29.
EXPERT SYSTEM TO REAL TIME CONTROL OF MACHINING PROCESSES. Lecture Notes in Computer Science. 2010. Vol: 5988. Pág. 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. AIP Conference Proceedings. 2009. Vol: 1181. Pág. 652-661.
ARCHITECTURE FOR THE OPTIMIZATION OF A MACHINING PROCESS IN REAL TIME THROUGH RULE-BASED EXPERT SYSTEM. AIP Conference Proceedings. 2009. Vol: 1181. Pág. 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. Lecture Notes in Computer Science. 2009. Vol: 5625. Pág. 106-121.
ACL2 VERIFICATION OF SIMPLICIAL DEGENERACY PROGRAMS IN THE KENZO SYSTEM. Lecture Notes in Computer Science. 2009. Vol: 5625. Pág. 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. Electronic Notes in Theoretical Computer Science. 2008. Vol: 200. Núm: 3. Pág. 87-102.
CONSTRUCTING FORMALLY VERIFIED REASONERS FOR THE ALC DESCRIPTION LOGIC. Electronic Notes in Theoretical Computer Science. 2008. Vol: 200. Núm: 3. Pág. 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. Lecture Notes in Computer Science. 2007. Vol: 4732. Pág. 135-150.
A FORMALLY VERIFIED PROVER FOR THE ALC DESCRIPTION LOGIC. Lecture Notes in Computer Science. 2007. Vol: 4732. Pág. 135-150.
Alonso-Jimenez, Jose Antonio;Aranda-Corral, Gonzalo Antonio;Martin-Mateos, Francisco Jesus:
KRRT: KNOWLEDGE REPRESENTATION AND REASONING TUTOR SYSTEM. Lecture Notes in Computer Science. 2007. Vol: 4739. Pág. 400-407.
KRRT: KNOWLEDGE REPRESENTATION AND REASONING TUTOR SYSTEM. Lecture Notes in Computer Science. 2007. Vol: 4739. Pág. 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. Journal of Automated Reasoning. 2006. Vol: 37. Núm: 1-2. Pág. 67-92.
FORMAL CORRECTNESS OF A QUADRATIC UNIFICATION ALGORITHM. Journal of Automated Reasoning. 2006. Vol: 37. Núm: 1-2. Pág. 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. IEEE Intelligent Systems and Their Applications. 2006. Vol: 21. Núm: 1. Pág. 42-52.
FOUNDATIONAL CHALLENGES IN AUTOMATED SEMANTIC WEB DATA AND ONTOLOGY CLEANING. IEEE Intelligent Systems and Their Applications. 2006. Vol: 21. Núm: 1. Pág. 42-52.
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. Lecture Notes in Computer Science. 2005. Vol: 3603. Pág. 358-372.
PROOF PEARL: A FORMAL PROOF OF HIGMAN S LEMMA IN ACL2. Lecture Notes in Computer Science. 2005. Vol: 3603. Pág. 358-372.
Palomo-Duarte, Manuel;Alonso-Jimenez, Jose Antonio;Martin-Mateos, Francisco Jesus:
RETE ALGORITHM APPLIED TO ROBOTIC SOCCER. Lecture Notes in Computer Science. 2005. Vol: 3643. Pág. 571-576.
RETE ALGORITHM APPLIED TO ROBOTIC SOCCER. Lecture Notes in Computer Science. 2005. Vol: 3643. Pág. 571-576.
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. Lecture Notes in Computer Science. 2004. Vol: 3018. Pág. 75-91.
FORMAL REASONING ABOUT EFFICIENT DATA STRUCTURES: A CASE STUDY IN ACL2. Lecture Notes in Computer Science. 2004. Vol: 3018. Pág. 75-91.
Alonso-Jimenez, Jose Antonio;Hidalgo-Doblado, Maria Jose;Martin-Mateos, Francisco Jesus;Ruiz-Reina, Jose Luis:
VERIFICATION OF THE FORMAL CONCEPT ANALYSIS. Revista de la Real Academia de Ciencias Exactas, Físicas y Naturales - Serie A: Matemáticas. 2004. Vol: 98. Núm: 1-2. Pág. 3-16.
VERIFICATION OF THE FORMAL CONCEPT ANALYSIS. Revista de la Real Academia de Ciencias Exactas, Físicas y Naturales - Serie A: Matemáticas. 2004. Vol: 98. Núm: 1-2. Pág. 3-16.
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. Journal of Automated Reasoning. 2004. Vol: 32. Núm: 4. Pág. 287-313.
FORMAL VERIFICATION OF A GENERIC FRAMEWORK TO SYNTHESIZE SAT-PROVERS. Journal of Automated Reasoning. 2004. Vol: 32. Núm: 4. Pág. 287-313.
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. Lecture Notes in Computer Science. 2004. Vol: 3040. Pág. 344-353.
FORMAL VERIFICATION OF MOLECULAR COMPUTATIONAL MODELS IN ACL2: A CASE STUDY. Lecture Notes in Computer Science. 2004. Vol: 3040. Pág. 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. Lecture Notes in Computer Science. 2003. Vol: 2850. Pág. 49-58.
A FORMAL PROOF OF DICKSON'S LEMMA IN ACL2. Lecture Notes in Computer Science. 2003. Vol: 2850. Pág. 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. Lecture Notes in Computer Science. 2003. Vol: 2664. Pág. 182-198.
VERIFICATION IN ACL2 OF A GENERIC FRAMEWORK TO SYNTHESIZE SAT-PROVERS. Lecture Notes in Computer Science. 2003. Vol: 2664. Pág. 182-198.
Ruiz-Reina, Jose Luis;Alonso-Jimenez, Jose Antonio;Hidalgo-Doblado, Maria Jose;Martin-Mateos, Francisco Jesus:
FORMAL PROOFS ABOUT REWRITING USING ACL2. Annals of Mathematics and Artificial Intelligence. 2002. Vol: 36. Núm: 3. Pág. 239-262.
FORMAL PROOFS ABOUT REWRITING USING ACL2. Annals of Mathematics and Artificial Intelligence. 2002. Vol: 36. Núm: 3. Pág. 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. Lecture Notes in Computer Science. 2002. Vol: 2509. Pág. 126-136.
SPECIFICATION OF ADLEMAN'S RESTRICTED MODEL USING AN AUTOMATED REASONING SYSTEM: VERIFICATION OF LIPTON'S EXPERIMENT. Lecture Notes in Computer Science. 2002. Vol: 2509. Pág. 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. Lecture Notes in Computer Science. 2001. Vol: 1930. Pág. 92-106.
FORMALIZING REWRITING IN THE ACL2 THEOREM PROVER. Lecture Notes in Computer Science. 2001. Vol: 1930. Pág. 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. Lecture Notes in Computer Science. 2001. Vol: 2178. Pág. 612-626.
VERIFYING AN APPLICATIVE ATP USING MULTISET RELATIONS. Lecture Notes in Computer Science. 2001. Vol: 2178. Pág. 612-626.
Martín-mateos, Francisco Jesús:
RAZONAMIENTO AUTOMÁTICO EN LÓGICAS POLIVALENTES MEDIANTE MÉTODOS ALGEBRAICOS EN MAPLE. TQ (Albacete). 1996. Vol: 3. Pág. 52-70.
RAZONAMIENTO AUTOMÁTICO EN LÓGICAS POLIVALENTES MEDIANTE MÉTODOS ALGEBRAICOS EN MAPLE. TQ (Albacete). 1996. Vol: 3. Pág. 52-70.
Tesis dirigidas o codirigidas
Serrano-suarez, Fabián Fernando:
FORMALIZACIÓN EN ISAR DE LA METALÓGICA DE PRIMER ORDEN. Tesis Doctoral. 2012
FORMALIZACIÓN EN ISAR DE LA METALÓGICA DE PRIMER ORDEN. Tesis Doctoral. 2012
