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)

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
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 Latex logo

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 SHiL.

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
SHiVTU source
SHiVWU source
SHiVCU source
SHiVTA source
SHiVWA source
SHiVCA source
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

  1. over 76 K-valid formulas provided by Heuerding
  2. over VTU/VWU/VCU/VTA-valid formulas
  3. over valid formulas obtained by the translations of the rules Rn,m of the sequent calculus for V
  4. over valid formulas in the style of Lewis’ axioms

The performances of tuCLEVER are promising and consistent with theorical expectations: in fact, hypersequent calculi SHiL 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.


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