wjzz avatar wjzz committed 1cdf813

Nitpick, nitpick.

Comments (0)

Files changed (1)

doc/final/index.tex

 
 The same argument can probably 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 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
 an insight into the importance of writing the inversion procedure in an efficient way :-)
 
 \subsubsection{Comparison within the lazy splitting group - Figure 4.}
 
-The full focusing prover always beats its less deterministic version, the weak focusing prover, as we expected,
-there is nothing to deep analysis.
+An we expected, the full focusing prover always beats its less deterministic version, the weak focusing prover.
+No deep thinking is required here.
 
-More interesting are differences to naive prover, which we suppose to be much worst than other provers.
+More interesting are differences to naive prover, which we suppose to be much worse than other provers.
 As mentioned in previous sections the tests Tensor with zeros and With with zeros are hard for our
 algorithms with lazy splitting due to non-deterministic choices.
 
 
 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,
-one for already inverted hypotheses and second for not.
+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,
+one for already inverted hypotheses and another for the remaiming ones.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
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.