我们问题的子句：{x，y}，{x，z}，{y，z}
我们如何才能从这些子句得出结论？
我可以看出，这是不能满足的，但我无法在分辨率证明系统中找到解决方案，因为似乎[｛x，y｝，｛｛-x，y｝]导致了｛x、y｝或｛y、x、x｝，然后我们可以导出{x，x｝和{y，y}。这似乎是显而易见的，因为(T或F(将永远是T。
我知道这是不令人满意的，因为没有解决方案可以满足这个问题。
您可以应用Davis-Putnam。这以一种详尽的方式应用解析，一次消除一个命题变量。当命题CNF公式不可满足时，可以推导出CCD_ 1。
这是一个很好的介绍https://www.fi.muni.cz/~popel/allens/collog/slides/davis-putnam.pdf。要生成证明，只需要跟踪它所做的有助于最终推导的分辨率。
对于这个问题，如果你按照x，y，z的顺序应用它，就会得到证明：
1. {x,y} . input
2. {x,z} . input
3. {y,z} . input
4. {~x,~y} . input
5. {~x,~z} . input
6. {~y,~z} . input
7. {y,~z} . resolve(x, 1, 5)
8. {~y,z} . resolve(x, 2, 4)
9. {~z} . resolve(y, 7, 6)
10. {z} . resolve(y, 3, 8)
11. {} . resolve(z, 10, 9)