VINTE: an Implementation of Internal Calculi for Lewis' Logics of Counterfactual Reasoning

Marianna Girlando (1, 2) , Bjoern Lellmann (3) , Nicola Olivetti (1, 2) , Gian Luca Pozzato (4) , Quentin Vitalis (5)

1 LIS - Laboratoire d'Informatique et des Systèmes (LIS) (Marseille, Toulon)
2 LIRICA - Logique, Interaction, Raisonnement et Inférence, Complexité, Algèbre
3 TU Wien - Vienna University of Technology = Technische Universität Wien
4 Dipartimento di Informatica [Torino]
5 École spéciale Militaire de Saint-Cyr - Départément d'Informatique

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 V and some of its significant extensions with axioms N, T, C, W and A. VINTE is inspired by the methodology of leanT A P and it is implemented in Prolog. The paper shows some experimental results, witnessing that the performances of VINTE are promising.

Domaines: Informatique [cs]

Marianna Girlando, Bjoern Lellmann, Nicola Olivetti, Gian Luca Pozzato, Quentin Vitalis. VINTE: an Implementation of Internal Calculi for Lewis' Logics of Counterfactual Reasoning. TABLEAUX 2017, Sep 2017, Brasilia, Brazil. pp.149-159. ⟨hal-01794382⟩