Tesis doctoral de Albert Rubio Gimeno
Esta tesis doctoral se centra en el estudio de mecanismos para realizar deduccion automatica en logica de primer orden con igualdad. La demostracion automatica de teoremas se esta aplicando actualmente en muchas areas de la informatica como son la ingenieria de software, las bases de datos o la inteligencia artificial. los resultados de la tesis se pueden dividir en: los considerados basicos, como son en la definicion de ordenes sobre terminos (o expresiones) en la resolucion de restricciones simbolicas, cuya utilidad va mas alla de su aplicacion en este trabajo; y les resultados en deduccion automatica, que incluye resultados de completitud refutacional para procesos de deduccion mediante clausulas con restricciones de igualdad (tambien llamadas estrategias basicas) y de orden, considerando ademas el predicado de igualdad como predefinido y dando la posibilidad de trabajar modulo alguna teoria equacional.
Datos académicos de la tesis doctoral «Automated deduction with constrained clauses«
- Título de la tesis: Automated deduction with constrained clauses
- Autor: Albert Rubio Gimeno
- Universidad: Politécnica de catalunya
- Fecha de lectura de la tesis: 01/01/1994
Dirección y tribunal
- Director de la tesis
- Robert Nieu Wenhuis
- Tribunal
- Presidente del tribunal: Fernando Orejas Valdés
- Leo Bachimair (vocal)
- María Alpuente Frasnedo (vocal)
- Pierre Jonannaud Jean (vocal)