将布尔逻辑表达式简化为 DNF 和 CNF（在 Haskell 中）答案

【问题标题】：Simplifying boolean logic expressions to DNF and CNF (in Haskell)将布尔逻辑表达式简化为 DNF 和 CNF（在 Haskell 中）
【发布时间】：2014-07-26 15:45:23
【问题描述】：

我了解有一些普遍接受的算法可以将给定的布尔逻辑表达式简化为 CNF 或 DNF。我找到了一些关于这类事情的网站，但没有什么可以真正用来围绕它构建 Haskell 程序。

这不是家庭作业，我也不是要求别人给我写代码 - 我只是在寻找某种可以帮助我构建函数的资源。

在我看来，我必须定义一个数据类型 Exp，它处理 Or Exp Exp、And Exp Exp、etc.、etc。然后建立标准“规则”（De Morgan's，Modus Ponens，Modus Tollens，你有什么）用于反复申请Exp，直到我到达我没有进一步的地方。

（因为我一直在玩 Agda etc.，所以我倾向于在将其翻译为 Agda 之前用 Haskell 编写所有内容。所以，是的，如果您更熟悉表达任何内容在阿格达，那我也会明白的。）

【问题讨论】：

你的想法是对的。如果您的Exp 仅是And 或Or，那么您实际上只需要德摩根定律之一（取决于您是否达到CNF 或DNF）。你的问题到底是什么？
如果你添加更多的操作，你只需要用and, or, not重写它们。它并没有真正增加复杂性。另外，我对规则感到困惑。你需要两个德摩根。你需要一个发行版。
我不知道有什么描述。您匹配每个构造函数，在子代上调用 toCNF 并组合结果。显然，toCNF (And a b) = And (toCNF a) (toCNF b)。您还需要为 De Morgan 匹配 Not (And a b) 和 Not (Or a b)。当然，匹配Or 是最有趣的部分，但这只是分发。如果您发现这具有挑战性，我建议您首先编写一个应用 De Morgan 的函数，直到所有否定都是文字。它更简单，但基本相同。
您可以尝试实施例如Tseitin transformation。有很多网站解释了它的工作原理。

标签： haskell functional-programming logic boolean-logic agda

【解决方案1】：

您实际上可以使用漂亮的hatt 包。它有 API 用于转换为 NNF、CNF 等。这是一些示例代码：

import Data.Logic.Propositional
import Data.Logic.Propositional.NormalForms

a = Variable (Var 'A')
b = Variable (Var 'B')
c = Variable (Var 'C')
d = Variable (Var 'D')

expression = Conjunction a (Disjunction b (Conjunction c d))

然后你可以在ghci 中玩expression：

λ> expression
(A ∧ (B ∨ (C ∧ D)))
λ> toCNF expression
(A ∧ ((B ∨ C) ∧ (B ∨ D)))

我建议你看一下包的来源，因为它不是很复杂。

【讨论】：