Il corso si propone di sviluppare le principali tecniche di ragionamento automatico, basate sia su metodi di saturazione e completamento, che su metodi di backtracking. Lo studente verrà tra l'altro introdotto all'utilizzo di alcuni strumenti quali superposition provers, SAT- e SMT-solvers, model finders, model-checkers. Sono previsti sbocchi applicativi sia verso l'algebra computazionale che verso la verifica di sistemi informatici. Il corso è indicato sia per gli studenti interessati a contenuti logico-matematici che per gli studenti interessati a contenuti informatici o più in generali applicativi.
- Docente titolare: Silvio Ghilardi