归结证明系统中的推导：如何从给定子句导出空子句？

初始子句集合如下：

• 子句1: {x, y}
• 子句2: {x, z}
• 子句3: {y, z}
• 子句4: {¬x, ¬y}
• 子句5: {¬x, ¬z}
• 子句6: {¬y, ¬z}

你之前直接对{x,y}和{¬x,¬y}归结得到的是永真式，这类子句对推导没有价值，需要换互补对组合推进：

1. 子句1与子句5归结：利用x和¬x的互补性，得到新子句7: {y, ¬z}
2. 子句7与子句3归结：利用¬z和z的互补性，得到新子句8: {y}
3. 子句8与子句4归结：利用y和¬y的互补性，得到新子句9: {¬x}
4. 子句9与子句2归结：利用¬x和x的互补性，得到新子句10: {z}
5. 子句10与子句6归结：利用z和¬z的互补性，得到新子句11: {¬y}
6. 子句8与子句11归结：利用y和¬y的互补性，直接导出空子句{}

这个过程的核心是优先选择能产生非永真式子句的互补对，避免一开始就选择会生成重言式的归结组合。

内容的提问来源于stack exchange，提问作者NightOowl