1. Denbora logikarako dedukzio metodo berriak garatu eta ezartzea, eta sistema erreaktiboak egiaztatzeko edo “model checking” metodorako duen aplikazio praktikoa.
2. Teknika automatiko berriak garatu eta ezartzea, lehen ordenako logikan (bereziki, Adimen-SUMOn) deskribatutako ontologiak arazoen konponbidean aplikatzeko.
3. Dedukzio metodo orokorrak garatzea grafo logiketarako, bide propietateak barne.

Ikertzaileak har ditzaketen lantaldeak ditugu MINECO eta UPV-EHUren proiektuetan.

Taldeak hainbat masterretan ematen du prestakuntza, software garapeneko metodo formalei buruz eta arrazoibide automatikoari eta erakusle automatikoen erabilerari buruz.

Izenburua: Métodos formales y algoritmos para el diseño de sistemas (FORMALISM)

Erakunde Finantzatzailea: CICYT (ERREF. TIN2007-66523)

Iraupena: 2008/01/01etik 2012/12/31ra (2014/12/31ra arte luzatua).

Izenburua: Logic, Reasoning and Complexity (LoReaCo)

Erakunde Finantzatzailea: Eusko Jaurlaritza (erref.-GV: S-PE12UN050).

Iraupena: 2012/01/01etik 2013/12/31ra.

Izenburua: Logic and Reasoning (LoRea).

Erakunde Finantzatzailea: UPV-EHU (erref. UPV-EHU GIU12/26).

Iraupena: 2012/11/01etik 2015/12/31ra.

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

Erakunde Finantzatzailea: CICYT (ERREF. TIN2013-46181-C2-2-R)

Iraupena:  2014/01/01etik 2017/12/31ra

Izenburua: Logic and Reasoning (LoRea).

Erakunde Finantzatzailea: UPV-EHU (erref. UPV-EHU GIU15/30).

Iraupena: 2015/12/01etik 2018/11/30era