Исчисление высказываний в питоне

Question

Я ищу модуль исчисления высказываний, который работает в Python.

Моим пользователям нужно ввести формулу в текстовой области, а затем я должен проверить, правильна она или нет.

Я не могу напрямую проверить, соответствует ли введенный текст правильному, поскольку он не учитывает перестановки или подобные вещи.

Существует ли такой модуль?

- ПРАВИТЬ-

Вот скриншот проекта (дизайн не завершен):

Answer 1

Я просто наткнулся на этот вопрос.не знаю, нужен ли ответ больше, но я бы предложил использовать SymPy:

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

Answer 2

Это не так уж сложно.Все, что вам нужно сделать, это либо (а) найти, либо (б) написать утилиту, которая принимает произвольное предложение и создает таблицу истинности.Затем для двух предложений все, что вам нужно сделать, это сгенерировать две таблицы истинности и проверить, что атомарные переменные и последний столбец совпадают во всех строках.

Это O (2 ^ n) в количествеатомные переменные, и предполагает, что каждое предложение содержит одинаковое количество атомных переменных.Если могут быть включены дополнительные бесполезные атомарные переменные (например, OR (b или NOT b) эквивалентно a), вам нужно дополнить таблицы истинности более простого предложения, чтобы получить одинаковое количество строк.Если разрешено использовать разные атомарные переменные, то это становится еще сложнее.

Вы не можете сделать лучше, чем O (2 ^ n), предполагая P! = NP, так как полиномиальное решение решило бы общую проблему выполнимостипо исчислению высказываний.

Чтобы сгенерировать таблицу истинности, вам нужно (а) сгенерировать список всех 2 ^ n перестановок значений истинности атомных переменных (множество способов сделать это) и (b) оценивать предложения для произвольных присваиваний истинным значениям атомных переменных.Тогда просто составьте обе таблицы и сравните.Voila!

Answer 3

A, B, C ... в представленном вами примере кажутся множествами , не предложения. можно рассуждать об этих типах утверждений, но не как насколько я вижу, логика высказываний.

семантически сравнивая эти утверждения, вот что Вы хотите здесь, потребуется более сложная логика, но более простой способ, возможно, будет переписать все заявления в форме, сопоставимой через простой текст сравнение. То есть игнорируя коммутативность, это Заявление

 (A ⋃ B) ⋂ C

будет таким же, как это утверждение

 C ⋂ (B ⋃ A)

, хотя это не идеальная настройка, поскольку быть эквивалентными заявлениями, которые не признаются, Процесс выяснения этого с использованием логической эквивалентности будет быть намного сложнее использование логики переписывания делает более или менее что вы хотите с очень небольшим усилием. в основном все вы необходимо указать, какие из бинарных операторов коммутативной. несколько уравнений, которые переписывают эквивалент Заявления также добавляются, возможно, вам придется добавить больше ... я написал что-то на Мод 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