Commit fb8dcacd authored by Łukasz Czajka's avatar Łukasz Czajka
Browse files

paper

parent b6edecde
......@@ -261,7 +261,9 @@ search is divided into two phases: the inversion phase and the
focusing phase. In the inversion phase, the rules are applied
eagerly. Backtracking is limited to the focusing phase and the choice
of focus. To avoid pointless choices, in an implementation one could
e.g.~store with each formula the set of its atomic targets.
e.g.~store with each formula the set of its atomic targets, or use
more sophisticated data structures allowing to perform the focusing
phase in ``one step''.
\smallskip
\noindent Inversion phase:
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment