VINTE

A theorem prover for Lewis' logics for counterfactual reasoning

A Prolog implementation of internal calculi for logic V and standard extensions

Check the validity of a conditional formula

Check the vaildity of a conditional formula




Conditional logic:    V    VN    VT    VW    VC    VA    VNA

Do NOT use capital letters for propositional variables. Use:

  • false for bottom
  • true for top
  • ^ for conjunction
  • ? for disjunction
  • - for negation
  • -> for material implication
  • => for conditional implication
  • < for comparative plausibility

Examples:

  • CPA: (a < a ? b) ? (b < a ? b)
  • TR: (a < b) ^ (b < c) -> (a < c)
  • CO: (a < b) ? (b < a)

Latex source file:

For compiling latex, download Adjustbox and Prooftree (prooftree.sty)

Prolog Source Code


Conditional Logic Axioms Characterizing Axiom Prolog Source Code
V CPR, CPA, TR, CO - code
VN CPR, CPA, TR, CO, N -(false < true) code
VT CPR, CPA, TR, CO, N, T (false < -a) -> a code
VW CPR, CPA, TR, CO, N, T, W a -> (a < true) code
VC CPR, CPA, TR, CO, N, T, W, C (a < true) -> a code
VA CPR, CPA, TR, CO, A1, A2
(a < b) -> (false < -(a < b))
-(a < b) -> (false < (a < b))
code
VNA CPR, CPA, TR, CO, N, A1, A2
-(false < true)
(a < b) -> (false < -(a < b))
-(a < b) -> (false < (a < b))
code

Experiments


We have compared VINTE with three theorem provers for conditional logics:

  • NESCOND - nested sequents for conditional logics
  • GoalDUCK - goal-directed proof search for conditional logics
  • CondLean - labelled sequent calculi for conditional logics

Performances of VINTE are promising, as witnessed by the following results obtained by testing the four provers over radomly genrated sequents.

The following tables show the number of timeouts over sequents with 100 formulas and a level of nesting 20 for logic V:

Theorem prover Time limit 5ms Time limit 1s
VINTE (for V) 45 0
CondLean 173 141
GoalDUCK 136 133
NESCOND 479 0

We have tested VINTE over 76 valid formulas, and compared its performance with those of NESCOND implementing internal calculi for conditional logics.

The following figure shows successes provided by the two provers within 1 ms (° are successes, - are timeouts):

In the next figure we show successes with a time limit of 3 minutes:

Valid formulas are obtained by translating modal logic K valid formulas provided by Heuerding in conditional formulas of conditional logic CK. NESCOND is faster, since it is specifically tailored for CK, but performance of VINTE are promising.



Prolog code

VINTE over random sequents: V - VN - VT - VW - VC - VA - VNA
VINTE vs NESCOND over valid formulas code

Authors

Marianna Girlando, Björn Lellmann,
Nicola Olivetti, Gian Luca Pozzato, Quentin Vitalis

with the valuable help of Cyril Terrioux

For questions and feedback, do not hesitate to contact us!

+39 011 670 68 48