Python中的命题演算

Question

我在找一个可以在Python中使用的命题演算模块。

我的用户需要在一个文本框里输入一个公式，然后我得检查这个公式是否正确。

我不能直接把用户输入的文本和正确的文本进行比较，因为这样没有考虑到排列组合之类的情况。

有没有这样的模块呢？

- 编辑 -

这是项目的截图（设计还没完成）：

Answer 1

在你给出的例子中，A、B、C看起来是集合，而不是命题。我们可以对这些类型的语句进行推理，但这不是用命题逻辑来做的，至少我认为是这样。

如果你想比较这些语句的语义，也就是它们的意思，那么需要用更复杂的逻辑来处理。不过，有一个更简单的方法，就是把所有语句改写成可以通过普通文本比较的形式。也就是说，忽略交换律，这个语句

 (A ⋃ B) ⋂ C

就和这个语句

 C ⋂ (B ⋃ A)

是一样的。虽然这种设置并不完美，因为可能会有一些等价的语句没有被识别出来，但用逻辑等价来搞清楚这一点会更加困难。使用改写逻辑基本上可以做到你想要的，而且花费的精力很少。基本上，你只需要指定哪些二元运算符是可交换的。还可以添加一些改写等价语句的方程，你可能需要添加更多的... 我在Maude上写了一些东西 http://maude.cs.uiuc.edu/

    mod VennDiagram is

    --- sorts
    sort Set .
    sort Statement .
    subsort Set < Statement .

    --- propositional formulas
    op a : -> Set .
    op b : -> Set .
    op c : -> Set .
    op d : -> Set .
    op e : -> Set .
    op f : -> Set .
    op g : -> Set .
    op h : -> Set .
    op i : -> Set .
    op j : -> Set .
    --- and so on ....

    --- connectives
    op ¬_  : Statement -> Statement .
    op _∁  : Statement -> Statement . --- complement
    op _∨_ : Statement Statement -> Statement [ comm ] .
    op _∧_ : Statement Statement -> Statement [ comm ] .
    op _↔_ : Statement Statement -> Statement [ comm ] .
    op _→_ : Statement Statement -> Statement .
    op _⋂_ : Statement Statement -> Statement [ comm ] .
    op _⋃_ : Statement Statement -> Statement [ comm ] .
    op _←_ : Statement Statement -> Statement .


    vars S1 S2 S3 S4 : Statement . --- variables

    --- simplify statemens through equivalence

    eq S1 → S2 = ¬ S1 ∨ S2 .
    eq S1 ↔ S2 = (S1 → S2) ∧ (S2 → S1) .
    eq ¬ ¬ S1 = S1 .
    eq S1 ← S2 = S2 → S1 .
    eq ¬ ( S1 ∧ S2 ) = (¬ S1) ∨ (¬ S2) .
    --- possibly other equivalences as well..

    endm

    --- check equality

    reduce a ↔ b == (b → a) ∧ (a → b) .
    reduce ¬ a ↔ ( a ∨ b ) ==  ¬ a ↔ ( b ∨ a ) .
    reduce (a ⋃ b) ⋂ c == c ⋂ (b ⋃ a) .

    --- what you need to do is to compare the right answer
    --- with a student answer through a simple comparison..
    --- reduce StudentAnswer == RightAnswer

Answer 2

我刚好看到这个问题。不知道现在还需要答案吗，但我建议可以使用SymPy：

http://docs.sympy.org/dev/modules/logic.html

Answer 3

这其实并不难。你只需要做两件事中的一件：(a) 找一个工具，或者 (b) 自己写一个工具，这个工具可以接收任意的命题，并生成一个真值表。然后，对于两个命题，你只需要生成两个真值表，检查所有行中的原子变量和最后一列是否匹配。

这个过程的复杂度是 O(2^n)，这里的 n 是原子变量的数量，并且假设每个命题包含相同数量的原子变量。如果有一些多余的无用原子变量（比如 a 或 (b 或 NOT b) 实际上等于 a），你需要在简单命题的真值表中填充额外的行，以确保行数相同。如果允许使用不同的原子变量，那就会变得更复杂。

假设 P 不等于 NP，你无法做到比 O(2^n) 更好的复杂度，因为一个多项式的解决方案会解决命题演算中的一般可满足性问题。

要生成真值表，你需要 (a) 生成所有 2^n 种原子变量真值的排列（有很多方法可以做到这一点），然后 (b) 对原子变量的任意真值分配来评估命题。最后，制作两个表并进行比较。就这样！