1. Desarrollo e implementación de nuevos métodos de deducción para lógicas temporales, y su aplicación práctica a la verificación de sistemas reactivos o "model checking".
2. Desarrollo e implementación de nuevas técnicas automáticas para la aplicación de ontologías descritas en lógica de primer orden (en particular de Adimen-SUMO) en resolución de problemas;
3. Desarrollo de métodos deductivos generales para lógicas de grafos incluyendo propiedades de caminos.

Tenemos proyectos MINECO y de la UPV-EHU a cuyos grupos de trabajo se pueden incorporar investigadores.

El grupo realiza formación en diversos másteres sobre metodos formales en el desarrollo de software y sobre razonamiento automático y el uso de demostradores automáticos.

Título: Métodos formales y algoritmos para el disño de sistemas (FORMALISM)

Entidad Financiadora: CICYT (REF. TIN2007-66523)

Duración: del 1-1-2008 al 31-12-2012 (prorrogado al 31-12-2014).

Título: Logic, Reasoning and Complexity (LoReaCo)

Entidad Financiadora: Gobierno Vasco ((ref.-GV: S-PE12UN050)

Duración: del 1-1-2012 al 31-12-2013.

 
Título: Logic and Reasoning (LoRea)

Entidad Financiadora:  UPV-EHU (ref UPV-EHU GIU12/26)

Duración: del 1-11-2012 al 31-12-2015.

Título:  Modelos y Métodos Computacionales para Datos Masivos Estructurados (Computational Models and Methods for Massive Structured Data) (COMMAS)

Entidad Financiadora:  CICYT (REF. TIN2013-46181-C2-2-R )

Duración: del 1-1-2014 al 31-12-2017.

Título:  Logic and Reasoning (LoRea)

Entidad Financiadora:  UPV-EHU (ref UPV-EHU GIU15/30)

Duración: 1-12-2015 al 30-11-2018.