【发布时间】：2014-09-27 09:28:47
【问题描述】：
输入是带有（任何）已检查语法的符号字符串，输出是 TRUE 或 FALSE。
我的想法是用 AND、XOR 和 TRUE 编写的逻辑表达式的 post-fix 表示，但我最终意识到这些模式在 post-fix 中将更难识别。
例子：
p IMPLIES 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
这个布尔环中的规则与普通代数中的规则相同，只有两条规则
- p+p=0
- pp=p
并且这些规则连同交换一起负责所有的减少，如果字符串对应于重言式，这将导致“1”。重言式 Modus ponens,
((p 暗示 q) AND 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。其他表达式减少为代数上更简单的表达式。
这是一个好的策略吗？计算机科学中使用了哪些策略？
【问题讨论】：
-
您在此提出的建议让人想起 1854 年乔治·布尔 (George Boole) 的“思想规律调查”中发表的布尔逻辑的开端。如果您有时间，这是一本引人入胜的读物。
-
谢谢！我在gutenberg.org/files/15114/15114-pdf.pdf 上找到了这本书，并会尝试阅读它。布尔环，其中每个表达式都只用 AND 和 XOR 放在形式上，这对于人类思维来说是非常反直觉的，但非常容易在代数上减少。
-
在可免费下载的程序 OTTER 中有一种方法可以确定格式正确的公式是否是重言式。 J. A. Kalman 的书“Automated Reasoning with OTTER”在第 1 页左右暗示了这一点。 342. 如果你给我发电子邮件到 Lefelhocz2@yahoo.com，我可以向你展示一个示例 OTTER 输入
-
@Dough：嗨！我对执行上面的程序最感兴趣，并且不认为命题重言式很难检查。大多数情况下，我对布尔环在逻辑上的作用感兴趣，就像上面的布尔书一样。还是谢谢你！
标签： logic boolean-logic algebra boolean-expression theorem-proving