3

I'm looking for a propositional calculus module that works in python.

My users need to input a formula in a text area, then I have to check whether it's correct or not.

I cannot directly test if the input text equals the correct one as it didn't take permutations or such things into account.

Does such a module exist ?

- EDIT -

Here is a screenshot of the project (design not complete) :

enter image description here

Improve this question
7
  • homework :) i've not heard of one, but writing one should not be that complex for propositional terms, writing a parsing for the input format is probably harder than writing the prover.. Commented Aug 18, 2011 at 9:28
  • Not homework directly. I'm developing an online homework platform, therefore I need to check students input. Commented Aug 18, 2011 at 9:36
  • ok, can you choose language and input format? Commented Aug 18, 2011 at 9:54
  • I've got a list of buttons which fill the input text with latex commands. So I can easily fill an invisible input text with an other set of characters to be parsed. See a screenshot in my post. Commented Aug 18, 2011 at 10:02
  • i see, so you can easily choose what you generate with those buttons. you basically want to see if student input is equivalent to what the actual answer should be? i.e. student_anwer <=> answer, using a prover? Commented Aug 18, 2011 at 10:18

3 Answers 3

Reset to default
1

This isn't too hard. All you need to do is to either (a) find or (b) write a utility that takes in an arbitrary proposition and produces a truth table. Then, for two propositions, all you need to do is to generate two truth tables and check that the the atomic variables and last column match in all rows.

This is O(2^n) in the number of atomic variables, and assumes that each proposition contains the same number of atomic variables. If extra useless atomic variables may be included (like a OR (b or NOT b) is equivalent to a), you will need to pad the truth tables of the simpler proposition in order to get the same number of rows. If different atomic variables are allowed to be used, then this gets even harder.

You cannot do better than O(2^n), assuming P != NP, since a polynomial solution would solve the general satisfiability problem over propositional calculus.

To generate a truth table, you need to (a) generate a list of all 2^n permutations of truth values of the atomic variables (lots of ways to do this), and (b) evaluate propositions for arbitary assignments to the truth values of atomic variables. Then just make both tables and compare. Voila!

Improve this answer
Sign up to request clarification or add additional context in comments.

4 Comments

It may be possible to gain some efficiency by generating the truth tables line-by-line (as it were) and stop as soon as a difference is found. That's not changing the time complexity, merely (on average) cutting it in, at a guess, half.
Good point. There may even be some other tricks you can use to make this pill a little less bitter...
if the UI is any indication, then the number of free variables is 4, A, B, C and D. 2^4 is a very small number (it's 16)
Another good point. Totally overlooked that. In that case, there's no excuse for not building a truth table.
1

i just stumpled upon this question. don't know if an answer is needed anymore, but I would suggest using SymPy:

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

Improve this answer

Comments

0

A, B, C... in the example you present seem to be sets, not propositions. it's possible to reason about these types of statements as well, but not as propositional logic, as far as I can see.

comparing these statements semantically, which is what you want here, would require a more complex logic, but an easier way would perhaps be to rewrite all statements to a form comparable through a plain text comparison. I.e. by ignoring commutativity, this statement

 (A ⋃ B) ⋂ C

would be the same as this statement

 C ⋂ (B ⋃ A)

even though this is not a perfect setup, since there might be equivalent statements which are not recognized, the process of figuring this out using logical equivalence would be much harder. using rewriting logic does more or less what you want with very little effort. basically all you need is to specify which of the binary operators which are commutative. a few equations which rewrite equivalent statements are also added, you may have to add more... i've written up something in 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
Improve this answer

Comments

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.