2018.6.14
引入回跳规则(BackJump Rule):
[
I
1
,
P
∘
,
I
2
]
∥
F
↪
[
I
1
,
ℓ
]
∥
F
,
(
C
→
l
)
i
f
{
[
I
1
,
P
∘
,
I
2
]
⊭
F
E
x
i
s
t
s
C
s
.
t
.
:
F
⇒
(
C
→
l
)
I
1
⊨
C
v
a
r
(
ℓ
)
u
n
d
e
f
.
i
n
I
1
v
a
r
(
ℓ
)
a
p
p
e
a
r
s
i
n
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
→
l
C\to l
C→l就叫做冲突子句，我们只要避免冲突子句就可以进一步寻找解。
