logic - 证明命题重言式的策略？

Question

输入是具有（任何）已检查语法的符号字符串，输出为 TRUE 或 FALSE。

我的想法是用 AND、XOR 和 TRUE 编写的逻辑表达式的 post-fix 表示，但我最终意识到在 post-fix 中这些模式将更难识别。

例子：

p 意味着 q可以写成TRUE XOR p (XOR (p AND q))缩写 1+p+pq

p EQUIVALENT WITH q可以简写为 1+p+q

NOT p缩写 1+p

p OR q缩写为 p+q+pq

这个布尔环中的规则与普通代数中的规则相同，有两个规则

并且这些规则连同交换一起负责所有减少，如果字符串对应于重言式，这将导致“1”。重言式 Modus ponens，

((p 暗示 q) 和 p) 暗示 q ,

应先如上代入，然后分布乘法展开，最后反复化简。直接替换 IMPLIES 给出：

1+((1+f+fg)f)+((1+f+fg)f)g =
= 1+ f+ff+fgf +(f+ff+fgf)g =
= 1+ f+f+fg + fg+fg+fg =
= 1+ fg +fg+fg+fg = 1

当一个重言式表达式被写成布尔环中的一个元素时，它会机械地归约为 1。其他表达式归约为代数上更简单的表达式。

这是一个好策略吗？计算机科学中使用了哪些策略？

score 2 · Accepted Answer

正如本概述论文中所讨论的，任意命题公式可以转换为合取范式( CNF )，使得它只有多项式更大的大小并且如果原始公式是重言式则不可满足。

从公式转换为 CNF 的实用工具包括bool2cnf和bc2cnf。

请参阅相关帖子，其中展示了如何使用 SAT 求解器处理命题公式。

1 回答 1