Metodi per il ragionamento automatico

L'insegnamento si propone di introdurre lo studente alle principali tecniche di ragionamento automatico, basate sia su tecniche di saturazione e completamento, che su tecniche di backtracking. Sono previsti sbocchi applicativi sia verso l'algebra computazionale che verso la verifica di sistemi informatici.

Saper utilizzare, conoscendone i principi di funzionamento, strumenti quali SMT-solvers e superposition provers.