989ee48
committed
Commits
Comments (0)
Files changed (1)

+5 4doc/final/index.tex
doc/final/index.tex
+The proof in the last example can be found using just the invertible rules. We difference comes from the
+fact that we have implemented an optimized version of the inversion procedure in the FullLS and WeakLS
+provers while we haven't done so in the Full version. Luckily, we can turn this communication mistake into
 $\m{forall}$ (P Q : $\m{Formula}$), $\m{isProvable}$ ( $  P \tensor Q \lolli Q \tensor P) $ == $\m{True}$%% TODO more latex here
+ $\m{forall}$ (P Q : $\m{Formula}$), $\m{isProvable}$ ( $  P \tensor Q \lolli Q \tensor P) $ == $\m{True}$