Línia de recerca: Deducció automàticaEstudi de fonaments per a la deducció automàtica en lògica de primer ordre amb igualtat i en lògica d'ordre superior. Sistemes de reescriptura.