L'area di questo progetto è il ragionamento automatico, o come far ragionare le macchine, non
necessariamente come gli umani, ma piuttosto a modo loro.
La deduzione automatica adotta metodi basati sulla logica, che ci offre un linguaggio con cui le
macchine possono ragionare. Si danno problemi di validità (ovvero se una congettura segue da un
insieme di assunzioni) o di soddisfacibilità (ovvero se un insieme di vincoli ammetta soluzione), dove
congettura, assunzioni, vincoli, sono formule logiche, che esprimono proprietà di un oggetto di studio
(per esempio un sistema, un programma, un tipo di dati, un circuito, un protocollo, una struttura
matematica). A un problema di validità si risponde con una prova o un contro-esempio. A un
problema di soddisfacibilità si risponde con una soluzione o una prova che non ne esistono.
Il tema di questo progetto è l'uso della semantica in deduzione automatica. La maggior parte dei
metodi più esplorati sin qui sono di natura primariamente sintattica. Questo progetto avanza un
diverso stile di ragionamento, che chiamiamo Guidato dalla Semantica e Sensibile al Goal, in breve
SGGS.
Le caratteristiche distintive di SGGS sono (a) una logica molto espressiva, la logica al prim'ordine; (b)
guida semantica da un'interpretazione iniziale, che dà alla macchina una nozione di vero o falso in
almeno uno stato del mondo; (c) sensibilità al goal, ovvero alla congettura da dimostrare; (d)
costruzione dinamica ed aggiornamento di un modello dell'insieme di clausole per cui si cerca una
prova; e (d) confluenza rispetto alla prova, che significa che non è necessario disfare passi già fatti e
tornare a uno stato precedente nella ricerca di una prova.
