Il gruppo di ricerca individua due fra gli innumerevoli approcci possibili alla riflessione sul ragionamento deduttivo: uno legato alla pratica quotidiana del pensiero dell'uomo comune e l'altro legato allo studio dell'evoluzione temporale di sistemi complessi.
Per quanto riguarda il primo approccio, intende considerare il ruolo della logica all’interno del ragionamento deduttivo, enucleando, sulla base anche della letteratura relativa alla psicologia del ragionamento, da un lato quello che dovrebbe essere tale ruolo e, dall’altro, le situazioni in cui tale ruolo non si realizza pienamente. Queste ultime verranno indagate relazionandole ai contesti conversazionali, cognitivi e deontici in cui hanno luogo, ponendo come obiettivo della ricerca un'unificazione fra le varie teorie del ragionamento deduttivo (teoria dei modelli mentali, teorie sensibili al contesto, teorie evoluzionistiche, teorie dualistiche), che permetta sia di spiegare l'origine degli errori nella pratica quotidiana sia di progettare nuove metodologie didattiche per ridurli.
Per quanto riguarda il secondo approccio, è noto che l'introduzione della dimensione temporale nel ragionamento sui sistemi reali richiede di considerare situazioni in cui le strutture classiche che rappresentano gli stati di cose nel fluire del tempo siano legate fra loro da una legge di evoluzione. Sorge così il problema del model-checking, ossia il problema di determinare la soddisfacibilità di formule della logica temporale in questo ambito, in cui si intrecciano fra loro compiti di ragionamento eterogenei. Un quadro teorico adatto alle applicazioni a sistemi a stati infiniti è stato già individuato in recenti articoli firmati da componenti del gruppo di ricerca, dove è stato suggerito un approccio totalmente simbolico e logico-deduttivo. Questa linea di ricerca innovativa ha già prodotto un primo prototipo (chiamato MCMT: 'Model Checker Modulo Theories'), raggiungibile alla pagina web http://homes.dsi.unimi.it/~ghilardi/mcmt. MCMT traduce in problemi di soddisfacibilità di formule senza quantificatori di teorie elementari tutti i test di punto fisso che sorgono nella verifica di formule della logica temporale. I test di soddisfacibilità vengono poi risolti tramite lo SMT-solver Yices sviluppato allo Stanford Research Insitute. I primi risultati sperimentali si sono dimostrati incoraggianti e si prevede di ampliare in modo sostanziale sia le funzionalità di MCMT sia gli aspetti teorici collegati, onde raggiungere una sempre maggiore consapevolezza degli intricati fenomeni soggiacenti che riguardano la logica temporale e la sua interazione con le teorie elementari. Lo scenario che si delinea in questo modo risulta denso di implicazioni teoretiche relative al ruolo della logica e del ragionamento nel governare la complessità, in particolare la complessità e l'imprevedibilità dei sistemi del mondo reale.