Commits

wjzz committed 989ee48

Added the missing benchmark explanation.

Comments (0)

Files changed (1)

doc/final/index.tex

 
 The same argument can propably be used to justify the outcome of the 4th benchmark in both Figures.
 
-The proof in the last example can be found using just the invertible rules. We don't know
-if there is a deep reason for the difference here. 
-%% TODO: check the order in which the rules are applied in Full and FullLS
+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
+an insight into the importance of writing the inversion procedure in an efficient way :-)
 
 \subsubsection{Comparison within the non-deterministic context management group - Figure 3.}
 
 These tools allow one to state a general property, say
 
 \begin{small}
-  $\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}$
 \end{small}
 
 \begin{small}
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.