Syntax: use **-**, **and**, **or**, **->** for propositional operators , **true** and **false** for ⊤ and ⊥ , **<** for comparativity plausibility operator and **low capital letters** for propositional symbols. You can also use **(** and **)** as well.

Example: (a < a or b) or (b < a or b)

Here you will get the result of the computation.

Your formula is syntactically incorrect or contains not valid characters. Remember to use low capital letters for propositional symbols!

tuCLEVER hasn't managed to prove your formula within the time limit of 10 seconds.

Do you want to know more about these logics? Take a look at this paper .

Logic | Hilbert-style sytem | Universal sphere model's peculiarities |
---|---|---|

VTU | CPR,CPA,TR,CO,N,T,U1,U2 | - |

VWU | CPR,CPA,TR,CO,N,T,U1,U2,W |
weak centering |

VCU | CPR,CPA,TR,CO,N,T,U1,U2,W,C |
centering |

VTA | CPR,CPA,TR,CO,N,T,U1,U2,A1,A2 |
absoluteness |

VWA | CPR,CPA,TR,CO,N,T,U1,U2,W,A1,A2 |
absoluteness + weak centering |

VCA | CPR,CPA,TR,CO,N,T,U1,U2,W,C,A1,A2 |
absoluteness + centering |

If a formula *F* is valid in a conditional logic L, then tuCLEVER is able to generate a .tex file containing the proof tree of ⇒ *F* in hypersequent calculus SH^{i}_{L}.

You need bussproofs.sty to compile the resulted .tex file.

Type of test | Source code |
---|---|

experiment 1 | source |

experiment 2 | source |

experiment 3 | source |

experiment 4 | source |

We have done several kind of experiments. We have tested tuCLEVER

- over 76 K-valid formulas provided by Heuerding
- over VTU/VWU/VCU/VTA-valid formulas
- over valid formulas obtained by the translations of the rules R
_{n,m}of the sequent calculus for V - over valid formulas in the style of Lewis’ axioms

The performances of tuCLEVER are promising and consistent with theorical expectations: in fact, hypersequent calculi SH^{i}_{L} provide non-optimal decision procedures for VTU and its extensions. In this respect, it is known that deciding satisfiability for conditional formulas in Lewis' logics with uniformity is EXPTIME-complete.

Aix Marseille University, France

Technische Universität Wien, Austria

Aix Marseille University, France

Università di Torino, Italia

Università di Torino, Italia