tuCLE𝕍ER

Total reflexivity and uniformity conditional Lewis logics theorem prover

Check your conditional formula

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)

Valid!

Tip

Here you will get the result of the computation.

Syntax Error!

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

Timeout!

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

Not valid!

Conditional logics with uniformity and reflexivity

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

Detailed proof trees in

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ⁱ_L.

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

tuCLEVER is entirely implemented in Prolog

Here you can find the source codes for all hypersequent calculi.

You need SWI-Prolog to run them.

Calculus	Source code
SHⁱ_VTU	source
SHⁱ_VWU	source
SHⁱ_VCU	source
SHⁱ_VTA	source
SHⁱ_VWA	source
SHⁱ_VCA	source

Type of test	Source code
experiment 1	source
experiment 2	source
experiment 3	source
experiment 4	source

Experiments

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ⁱ_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.

Authors

Marianna Girlando

Aix Marseille University, France

Björn Lellmann

Technische Universität Wien, Austria

Nicola Olivetti

Aix Marseille University, France

Stefano Pesce

Università di Torino, Italia

Gian Luca Pozzato

Università di Torino, Italia