Logiche Condizionali: sviluppo di un Theorem Prover per Estensioni del Sistema CK

L’oggetto principale della mia tesi di laurea `e stato lo sviluppo di un Theorem Prover per il sistema di logiche condizionali normali CK e il cubo formato da 3 delle sue principali estensioni, ID, MP e CEM. Un Theorem Prover `e un software che implementa un algoritmo in grado di verificare la validità di una formula all’interno di un sistema logico: una formula è valida se è sempre vera, indipendentemente dal valore che si assegna agli elementi che la compongono. Le logiche condizionali sono un’estensione della logica proposizionale classica tramite l’aggiunta dell’operatore condizionale ⇒, che permette di catturare un ragionamento ipotetico, per cui l’implicazione logica classica → non `e adatta. Il risultato finale del mio lavoro `e una serie di 8 theorem prover, ciascuno con regole studiate ad hoc per il sistema logico in cui operano, e di conseguenza prestazioni notevoli anche per formule complesse e con alti livelli di annidamento.