Commits

wjzz committed df322da

Prover introduction nitpicks.

Comments (0)

Files changed (1)

doc/final/index.tex

 
 This document is an extension of the progress report previously submitted. 
 
-Since the last time, we have concentrated on making sure that our provers are correct and possibly memory efficient. 
+Since the last time, we have concentrated on making sure that our provers are correct and not horribly inefficient. 
 In this document we describe two families of provers that we have implemented and present some of the issues that have emerged in the process. 
 Next we show the results of benchmarking and explain our approach to testing the implementations. We conclude by discussing some ideas
 that didn't work out for us.
 
 \paragraph{Naive}
 
-The Naive provers implement a proof search with no optimalizations at all 
+The Naive provers implement a proof search with no optimizations at all 
 - at any point during the proof building process every applicable rule is tried in succession.
 
 It was easy to go from no context management to lazy splitting in this variant.
 
-These two flavors throw some light onto the impact resource management on performance. 
-%% TODO: this need to be elaborated, this _impact_ has to be either detailed or not mentioned whatsoever
-
 \paragraph{Weak}
 
-The Weak provers are a bit artificial, we intentionally introduce more non-determinism into algorithms
-to obtain implementation which strongly differ in behavior from full-focusing provers.
+The Weak provers implement chaining (weak focusing) and they are a bit artificial.
+We intentionally introduced more non-determinism into the implementation to make sure that the result is not simply a prover based on full-focusing.
+This approach seems a bit unnatural, because it is very tempting to add at least some inversion to a prover based on chaining.
 
-Implementation of weak-focusing prover with lazy splitting was done
-independently from first prover, so some difference of architectures
-can also influence performance.
+The implementation of weak-focusing prover with lazy splitting was done
+independently from first prover, so some difference in architectures
+can result in performance differences.
 
 \paragraph{Full}
 
-The second prover which implements lazy splitting is developed from
-the weak-focusing prover. Some performance optimizations are done
-here, what makes two implementations of full-focusing
-more similar. More is described in the next section.No mus
+The prover which implements lazy splitting is based on the weak-focusing prover. 
+Some performance optimizations are done here, what makes the two implementations of full-focusing
+more similar. A more detailed description follows.
 
 \subsection{Architecture of Naive, Weak and Full}
 
 Operator merges only final results of function, what for the \verb|Maybe| data type  means
 that we get first positive result of whole computation.
 
-\subsection{The copy rule and the positive atom optimalization}
+\subsection{The copy rule and the positive atom optimization}
 
 In one of the provers we have implemented a version of the \verb|copy| rule that permits focusing on
 a positive literal (and accordingly the \verb|id| rule for positive atoms in the persistent context