Trabajo de Lógica Computacional en Saarbrücken (Alemania)

El Grupo de automatización de la Lógica (del Instituto Max Planck en Saarbrücken, Alemania) ha publicado un anuncio de ofertas de plazas.

La investigación del grupo se centra en la deducción automática en fragmentos de la lógica de primer orden.

Desde el punto de vista teórico trabajan en el desarrollo, análisis y combinación de cálculos lógicos.

Desde el punto de vista práctico trabajan en la implementación de demostradores automáticos de teoremas y otros sistemas deductivos y su aplicación a la verificación asistida por computador de software y hardware.

Algunos de los sistemas que desarrolla el grupo son SPASS, SPASS+T y Waldmeister