- 消解反演：证明真或假
- 反演求解：求解变量值
消解反演解法：
1.否定命题，将否定后的命题加入前提
2.通过前提之间互相组合，得到新的前提
3.最终前提与前提互相矛盾，得到NIL，此时证明完成
注：在第1步之后第2步之前，还需要将所有的命题转换成子句形式
例1：
设已知：
（1）能阅读的人是识字的
（2）海豚不识字
（3）有些海豚是很聪明的
请用消解反演证明：有些很聪明的人并不能阅读
解1：
本体需要证明命题有些很聪明的人并不能阅读，是一个证明问题，而非求解。因此可以使用消解反演。
设谓词：
\(R(x):x能阅读\)
\(L(X):x识字\)
\(D(X):x是海豚\)
\(S(X):x聪明\)
前提：
- \(\forall x(R(x)\rightarrow D(x))\)
- \(\forall x(D(x)\rightarrow \neg L(x))\)
- \(\exists x(D(x)\wedge S(x))\)
结论：
- \(\exists x(S(x)\wedge \neg R(x))\)
消解反演：
结论的否定可以在任意时候加入组合，因此消解反演过程不止一种。下面展示其中一种求解过程。
a：常量，特指某条海豚
v：同$\vee$，合取
^：同$\wedge$，析取
~S(x)vL(x) D(a)^S(a)
│ │
│ │
│ │
└──────┬──────┘
│
│
│
D(a)^L(a) ~D(x)v~L(x)
│ │
│ │
│ │
└──────┬──────┘
│
│
│
NIL