python - python中的命题演算

Question

我正在寻找一个在 python 中工作的命题演算模块。

我的用户需要在文本区域输入公式，然后我必须检查它是否正确。

我无法直接测试输入文本是否等于正确的文本，因为它没有考虑排列或此类事情。

这样的模块存在吗？

- 编辑 -

这是项目的截图（设计不完整）：

Answer 1

我只是偶然发现了这个问题。不知道是否需要答案，但我建议使用 SymPy：

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

Answer 2

这不是太难。您需要做的就是 (a) 查找或 (b) 编写一个实用程序，该实用程序接受任意命题并生成真值表。然后，对于两个命题，您需要做的就是生成两个真值表并检查原子变量和最后一列是否在所有行中匹配。

这是原子变量数量的 O(2^n)，并假设每个命题包含相同数量的原子变量。如果可能包含额外的无用原子变量（如 OR (b or NOT b) 等价于 a），则需要填充更简单命题的真值表以获得相同的行数。如果允许使用不同的原子变量，那么这将变得更加困难。

假设 P != NP，你不能做得比 O(2^n) 更好，因为多项式解决方案将解决命题演算上的一般可满足性问题。

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

Answer 3

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