Francisco Jesús Martín Mateos

Profesor Titular de Universidad
fjesus@us.es
Área de conocimiento: Ciencia de la Computación e Inteligencia Artificial
Departamento: Ciencias de la Comput. e Int. Artificial
Grupo: LOGICA, COMPUTACION E INGENIERIA DEL CONOCIMIENTO (TIC-137)
Instituto de Inv.: I3US
Prog. doctorado: Programa de Doctorado en Ingeniería Informática (RD. 99/2011)
Tipo Año Título Fuente
Ponencia2017 Using abstract stobjs in ACL2 to compute matrix normal forms Lecture Notes in Computer Science
Ponencia2016 Future and emergent trends in language technology: First international workshop, FETLT 2015 Seville, Spain, november 19–20, 2015 revised selected papers Lecture Notes in Computer Science
Editorial2016 Preface Lecture Notes in Computer Science
Ponencia2016 Towards a verifiable Topology of Data XV Encuentro de Álgebra computacional y aplicaciones: EACA 2016
Artículo2015 Modelling algebraic structures and morphisms in ACL2 APPLICABLE ALGEBRA IN ENGINEERING COMMUNICATION AND COMPUTING
Ponencia2014 Artificial intelligence and symbolic computation: 12th international conference, AISC 2014 Seville, Spain, December 11-13, 2014 proceedings Lecture Notes in Computer Science
Artículo2014 Formally Verified Tableau-Based Reasoners for a Description Logic JOURNAL OF AUTOMATED REASONING
Editorial2014 Preface Lecture Notes in Computer Science
Artículo2014 Verifying the bridge between simplicial topology and algebra: the Eilenberg-Zilber algorithm Logic Journal of the IGPL
Ponencia2013 Certified symbolic manipulation: Bivariate simplicial polynomials Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC
Artículo2012 Formalization of a normalization theorem in simplicial topology ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE
Ponencia2011 Applying ACL2 to the formalization of algebraic topology: Simplicial polynomials Lecture Notes in Computer Science
Capítulo2011 Computational logic and knowledge representation issues in data analysis for the semantic web Data Management in the Semantic Web
Artículo2011 Proof Pearl: a Formal Proof of Higman's Lemma in ACL2 JOURNAL OF AUTOMATED REASONING
Ponencia2010 Expert System to Real Time Control of Machining Processes CURRENT TOPICS IN ARTIFICIAL INTELLIGENCE
Capítulo2010 Topología simplicial en ACL2 Contribuciones científicas en honor de Mirian Andrés Gómez
Ponencia2009 ACL2 verification of simplicial degeneracy programs in the kenzo system INTELLIGENT COMPUTER MATHEMATICS, PROCEEDINGS
Ponencia2009 Verificación y eficiencia en programas para el cálculo simbólico: estudio de un caso Programación y lenguajes: IX Jornadas sobre Programación y Lenguajes, PROLE'09, I Taller de Programación Funcional, TPF'09, San Sebastián, España, del 8 al 11 de septiembre de 2009
Ponencia2007 A formally verified prover for the ALC description logic THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS
Ponencia2007 A formally verified prover for the ALC description logic Lecture Notes in Computer Science
Ponencia2007 KRRT: Knowledge Representation and Reasoning Tutor system COMPUTER AIDED SYSTEMS THEORY- EUROCAST 2007
Ponencia2007 KRRT: Knowledge representation and reasoning tutor system Lecture Notes in Computer Science
Artículo2006 Formal correctness of a quadratic unification algorithm JOURNAL OF AUTOMATED REASONING
Artículo2006 Foundational challenges in automated Semantic Web data and ontology cleaning IEEE INTELLIGENT SYSTEMS
Ponencia2005 Proof pearl: A formal proof of Higman's Lemma in ACL2 Lecture Notes in Computer Science
Artículo2005 Proof pearl: A formal proof of Higman's lemma in ACL2 THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS
Artículo2005 Rete algorithm applied to robotic soccer COMPUTER AIDED SYSTEMS THEORY - EUROCAST 2005
Ponencia2005 Rete algorithm applied to robotic soccer Lecture Notes in Computer Science
Capítulo2005 Topología Simplicial en ACL2 Manual de responsabilidad pública: homenaje a Pedro González Gutiérrez-Barquín
Artículo2004 Formal reasoning about efficient data structures: A case study in ACL2 Lecture Notes in Computer Science
Artículo2004 Formal verification of a generic framework to synthesize SAT-provers JOURNAL OF AUTOMATED REASONING
Ponencia2004 Formal verification of molecular computational models in ACL2: A case study Lecture Notes in Computer Science
Artículo2003 A formal proof of Dickson's Lemma in ACL2 LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS
Artículo2003 Verification in ACL2 of a generic framework to synthesize SAT-provers LOGIC BASED PROGRAM SYNTHESIS AND TRANSFORMATION
Artículo2002 Formal proofs about rewriting using ACL2 ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE
Capítulo2001 Formalización del razonamiento ecuacional en una lógica computacional Actas del Encuentro de Matemáticos Andaluces
Ponencia2001 Formalizing rewriting in the ACL2 theorem prover Lecture Notes in Computer Science
Artículo2001 Formalizing rewriting in the ACL2 theorem prover ARTIFICIAL INTELLIGENCE AND SYMBOLIC COMPUTATION
Artículo2001 Verifying an applicative ATP using multiset relations COMPUTER AIDED SYSTEMS THEORY - EUROCAST 2001
Ponencia2001 Verifying an applicative ATP using multiset relations Lecture Notes in Computer Science

Proyectos de Investigación

Fecha de inicio Fecha de fin Rol Denominación Agencia financiadora
28/12/2000 27/12/2003 Investigador/a Desarrollo y verificación formal de sistemas de razonamiento (TIC2000-1368-C03-02) Ministerio de Ciencia y Tecnología (Nacional)
01/01/2014 31/12/2017 Investigador/a Lógica Computacional para la Ciencia del Dato (TIN2013-41086-P) Ministerio de Economía y Competitividad (Nacional)
01/01/2010 31/12/2010 Investigador/a Gestión mecanizada del conocimiento matemático. Aplicaciones en lógica (MTM2009-13842-C02-02) Ministerio de Ciencia e Innovación (Nacional)
13/12/2004 13/12/2007 Investigador/a Sistemas verificados para razonamiento en la Web semántica (TIN2004-03884) Ministerio de Ciencia y Tecnología (Nacional)

Contratos

Fecha de inicio Fecha de fin Rol Denominación Agencia financiadora
01/01/2011 30/05/2011 Responsable Informe técnico sobre aplicabilidad de Sistemas Basados en el Conocimiento al proyecto SOLEME (P025-11/E19) Clever Tecnología S.L. (Local)