Sviluppo di un theorem prover per logiche condizionali di Lewis con uniformità e riflessività

David Lewis ha proposto una formalizzazione delle logiche condizionali con l'intento di catturare i contraffattuali, ovvero quei condizionali al congiuntivo che ricalcano lo schema “Se fosse stato il caso di ... allora sarebbe stato il caso di ...”. Quando pronunciamo frasi di questo tipo, sottintendiamo in genere che l'antecedente è falso. Per questo motivo, i contraffattuali non possono essere efficacemente espressi per mezzo dell'implicazione materiale, in quanto risulterebbero banalmente sempre veri. In questa tesi presentiamo tuCLEVER, un theorem prover per la logica condizionale VTU e le sue estensioni VWU, VCU, VTA, VCA e VWA.