73 well. In that case there is really no fundamental difference between |
73 well. In that case there is really no fundamental difference between |
74 the two kinds of assumptions, apart from the order of reducing the |
74 the two kinds of assumptions, apart from the order of reducing the |
75 individual parts of the proof configuration. |
75 individual parts of the proof configuration. |
76 |
76 |
77 Nevertheless, the ``strong'' mode of plain assumptions is quite |
77 Nevertheless, the ``strong'' mode of plain assumptions is quite |
78 important in practice to achieve robustness of proof document |
78 important in practice to achieve robustness of proof text |
79 interpretation. By forcing both the conclusion \emph{and} the |
79 interpretation. By forcing both the conclusion \emph{and} the |
80 assumptions to unify with the pending goal to be solved, goal |
80 assumptions to unify with the pending goal to be solved, goal |
81 selection becomes quite deterministic. For example, decomposition |
81 selection becomes quite deterministic. For example, decomposition |
82 with ``case-analysis'' type rules usually give rise to several goals |
82 with rules of the ``case-analysis'' type usually gives rise to |
83 that only differ in there local contexts. With strong assumptions |
83 several goals that only differ in there local contexts. With strong |
84 these may be still solved in any order in a predictable way, while |
84 assumptions these may be still solved in any order in a predictable |
85 weak ones would quickly lead to great confusion, eventually demanding |
85 way, while weak ones would quickly lead to great confusion, |
86 even some backtracking. |
86 eventually demanding even some backtracking. |
87 *}; |
87 *}; |
88 |
88 |
89 end; |
89 end; |