VINTE: An implementation of internal calculi for lewis'€ logics of counterfactual reasoning

We present VINTE, a theorem prover for conditional logics for counterfactual reasoning introduced by Lewis in the seventies. VINTE implements some internal calculi recently introduced for the basic system and some of its significant extensions with axioms ℕ , , ℂ , and . VINTE is inspired by the methodology of lean and it is implemented in Prolog. The paper shows some experimental results, witnessing that the performances of VINTE are promising.