2018.6.14 引入回跳规则(BackJump Rule):[I1,P∘,I2]∥F↪[I1,ℓ]∥F,(C→l) if{[I1,P∘,I2]⊭FExists C s.t.:F⇒(C→l)I1⊨Cvar(ℓ) undef. in I1var(ℓ) appears in F[I_1,P^{\circ},I_2]\lVert F\hookrightarrow [I_1,\ell]\lVert F, (C\to l)~if \begin{cases}[I_1,P^{\circ},I_2]\not\models F\\ Exists~C~s.t.:F\Rightarrow (C\to l)\\ I_1\models C\\ var(\ell)~undef.~in~I_1\\ var(\ell)~appears~in~F\end{cases}[I1,P∘,I2]∥F↪[I1,ℓ]∥F,(C→l) if⎩⎪⎪⎪⎪⎪⎪⎨⎪⎪⎪⎪⎪⎪⎧[I1,P∘,I2]⊨FExists C s.t.:F⇒(C→l)I1⊨Cvar(ℓ) undef. in I1var(ℓ) appears in F 这里C→lC\to lC→l就叫做冲突子句，我们只要避免冲突子句就可以进一步寻找解。 相关文章：
