María José Hidalgo Doblado

Profesora Titular de Universidad
mjoseh@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)
Prog. doctorado: Programa de Doctorado en Ingeniería Informática (RD. 99/2011)
Tipo Año Título Fuente
Artículo2018 A logic-algebraic tool for reasoning with Knowledge-Based Systems JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING
Artículo2014 Formally Verified Tableau-Based Reasoners for a Description Logic JOURNAL OF AUTOMATED REASONING
Artículo2011 Proof Pearl: a Formal Proof of Higman's Lemma in ACL2 JOURNAL OF AUTOMATED REASONING
Artículo2008 Constructing Formally Verified Reasoners for the ALC Description Logic ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE
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
Artículo2006 Formal correctness of a quadratic unification algorithm JOURNAL OF AUTOMATED REASONING
Artículo2005 Proof pearl: A formal proof of Higman's lemma in ACL2 THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS
Ponencia2005 Proof pearl: A formal proof of Higman's Lemma in ACL2 Lecture Notes in Computer Science
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
Ponencia2001 Verifying an applicative ATP using multiset relations Lecture Notes in Computer Science
Artículo2001 Verifying an applicative ATP using multiset relations COMPUTER AIDED SYSTEMS THEORY - EUROCAST 2001
Ponencia1997 Sobre la enseñanza de la lógica Actas del I Congreso de la Sociedad de Lógica, Metodología y Filosofía de la Ciencia en España: [Madrid 15,16 y 17 de diciembre de 1993]
Este investigador no ha dirigido/tutorizado tesis

Proyectos de Investigación

Fecha de inicio Fecha de fin Rol Denominación Agencia financiadora
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)
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/06/2020 31/05/2023 Investigador/a Herramientas Lógicas y Algebraicas para el Análisis de Sistemas Basados en Conocimiento. Aplicaciones (PID2019-109152GB-I00) Ministerio de Ciencia, Innovación y Universidades (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)