This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
reference:drule [2011/06/22 12:29] 131.246.161.187 |
reference:drule [2011/07/06 12:08] (current) 131.246.161.187 |
||
---|---|---|---|
Line 14: | Line 14: | ||
* [[unification|Unify]] $P_1$ and $A_j$ for some $j$. The application fails if there is no unifier for any $j$; otherwise, let $U$ be this unifier. | * [[unification|Unify]] $P_1$ and $A_j$ for some $j$. The application fails if there is no unifier for any $j$; otherwise, let $U$ be this unifier. | ||
* Remove the old subgoal and create new ones: | * Remove the old subgoal and create new ones: | ||
- | * $\quad\bigwedge x_1 \dots x_k : [|\ U(A_1); \dots U(A_{j-1}); U(A_{j+1}); \dots ; U(A_m)\ ; U(Q) |] \Longrightarrow U(C)$ | + | * $\quad\bigwedge x_1 \dots x_k : [|\ U(A_1); \dots ; U(A_{j-1}); U(A_{j+1}); \dots ; U(A_m)\ ; U(Q) |] \Longrightarrow U(C)$ |
- | * $\quad\bigwedge x_1 \dots x_k : [|\ U(A_1); \dots U(A_{j-1}); U(A_{j+1}); \dots ; U(A_m)\ |] \Longrightarrow U(P_k)$ \\ for each $k = 2, \dots, n$. | + | * $\quad\bigwedge x_1 \dots x_k : [|\ U(A_1); \dots ; U(A_{j-1}); U(A_{j+1}); \dots ; U(A_m)\ |] \Longrightarrow U(P_k)$ \\ for each $k = 2, \dots, n$. |
+ | |||
+ | Note that ''drule'' is almost the same as ''[[frule]]''. The only difference is that ''frule'' keeps the assumption "used" by the used rule $A_j$ while ''drule'' drops it. This is useful if $A_j$ is needed to prove the new subgoals; ''drule'' is unsafe because of this. | ||
==== Example ==== | ==== Example ==== |