Theorem Proving for Lewis Logics of Counterfactual Reasoning.

We present tuCLEVER, a theorem prover for the strongest conditional logics of counterfactual reasoning introduced by Lewis in the seventies. tuCLEVER implements some hypersequent calculi recently introduced for the system VTU and its main extensions. tuCLEVER is inspired by the methodology of leanT^AP and it is implemented in Prolog. Preliminary experimental results show that the performances of tuCLEVER are promising.