A Prolog implementation of internal calculi for logic V and standard extensions
Check the validity of a conditional formulaConditional 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 

code  
VNA  CPR, CPA, TR, CO, N, A1, A2 

code 
We have compared VINTE with three theorem provers 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.
VINTE over random sequents: V 
VN 
VT 
VW 
VC 
VA 
VNA
VINTE vs NESCOND over valid formulas code
For questions and feedback, do not hesitate to contact us!
+39 011 670 68 48