我正在 youtube 上观看有关分辨率的视频，并看到了这个视频，它对我有很大帮助：
http://www.youtube.com/watch?v=hhTxW5c3BXo
接近尾声时，他做了一个例子，其中每个子句中相对侧的 X 都被抵消，其余的被连接在一起，这没关系，但我想知道它是否适用于多个变量抵消，例如：
(AB -> CDXY) (PQXY -> RS)
取消 XY 将给出 ABPQ -> RSCD
我有这种直觉，这种“双重分辨率”的情况不适用，而且我无法找到任何有关取消 2 个或更多变量的信息。
有什么我想念的吗？
将其称为“取消”对我来说似乎很奇怪，但是是的，您示例中的 XY 以您希望的方式运行。
请不要陷入仅以代数方式操作符号的陷阱。如果你要学习这些东西，你必须能够思考所有这些符号的含义。在这种情况下，您要问的是...
Given that (A&B) implies (C&D&X&Y)
and that (P&Q&X&Y) implies (R&S)
can you deduce that (A&B&P&Q) implies (R&S&C&D)?
你能看出 (A&B) 必须暗示 (C&D) 并且 (A&B) 也必须暗示 (X&Y) 吗？并且当您将 (P&Q) 添加到混合中时，是否存在从 (A&B) 到 (X&Y) 再到 (R&S) 的推理链？
并不是对 XY 的一个引用抵消了对 XY 的另一个引用，而是 XY 充当垫脚石的方式类似于 M 在参数 L->M、M->N、因此 L->N 中所做的事情。
另一种考虑它的方式是关于命名。X 和 Y 代表一些真值泛函命题。谁决定一个叫 X 而另一个叫 Y？我们没有理由不能把这两个命题放在一起作为一个单一的合取并称之为 Z。那么你的两个前提包含一个变量 Z 而不是复合 XY。如果你想这样想，Z 可以“取消”。