User Tools
reference:drule
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
|
reference:drule [2011/06/22 12:34] 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. | 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. | ||
reference/drule.1308738892.txt.gz · Last modified: 2011/06/22 12:34 by 131.246.161.187
Page Tools
