1cdf813
committed
Commits
Comments (0)
Files changed (1)

+8 8doc/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
+Inversion by itself is sufficient to find the proof in the last example. The 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
The full focusing prover always beats its less deterministic version, the weak focusing prover, as we expected,
+An we expected, the full focusing prover always beats its less deterministic version, the weak focusing prover.
More interesting are differences to naive prover, which we suppose to be much worstthan other provers.
+More interesting are differences to naive prover, which we suppose to be much worse than other provers.
However, this disadvantage of basic lazy splitting does not explain why the Naive prover is almost twice
better than the FullLS prover at the test Tensor commutativity. It shows defect of our implementation.
The FullLS (and the WeakLS) prover tries to make possible inversions after each recursive call, but
context is fully decomposed into atoms at beginning. It means that after each step whole context would be
analyzed for possible inversions. We can solve this problem by splitting input resources into two sets,
+The FullLS (and the WeakLS) prover tries to make all possible inversions after each recursive call, but here
+the context is fully decomposed into atoms at the beginning. It means that after each step whole context would be
+analyzed for possible inversions. We could solve this problem by splitting input resources into two sets,
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%