User Tools
reference:drule
Differences
This shows you the differences between two versions of the page.
| Next revision | Previous revision | ||
|
reference:drule [2011/06/22 12:20] 131.246.161.187 created |
reference:drule [2011/07/06 12:08] (current) 131.246.161.187 |
||
|---|---|---|---|
| Line 7: | Line 7: | ||
| $\quad\bigwedge x_1 \dots x_k : [|\ A_1; \dots ; A_m\ |] \Longrightarrow C$ | $\quad\bigwedge x_1 \dots x_k : [|\ A_1; \dots ; A_m\ |] \Longrightarrow C$ | ||
| - | and we want to use ''rule'' with rule | + | and we want to use ''drule'' with rule |
| $\quad[|\ P_1; \dots ; P_n\ |] \Longrightarrow Q$ | $\quad[|\ P_1; \dots ; P_n\ |] \Longrightarrow Q$ | ||
| 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 ==== | ||
reference/drule.1308738008.txt.gz · Last modified: 2011/06/22 12:20 by 131.246.161.187
Page Tools
