Wednesday, 20 July 2011

Tree Proof Generator

When I used to teach elementary logic (Logic 1), I used to recommend students that they try using the online Tree Proof Generator, which will generate tableau proofs, or provide countermodels.

For example, given the valid formula $\forall x(Rxx \rightarrow \exists y Rxy)$, it gives the following tableau proof:
1. $\neg \forall x(Rxx \rightarrow \exists y Rxy)$
2. $\neg (Raa \rightarrow \exists yRay)$
3. $Raa$
4. $\neg \exists yRay$
5. $\neg Raa$
Published by at
Labels:

6 comments:

  1. Shouldn't the last line (5) read "$\neg Raa$"?

    ReplyDelete

  3. I'm trying to implement an automated tree proof generator for formulae of propositional logic. Do you know any sources where one could find tips on how to implement a proof generator like the one you've linked to?

    ReplyDelete

  5. Can you help me figure this problem out?

    :((P --> Q) V (Q --> R))

    ReplyDelete

  6. 1. $\neg (P \rightarrow Q) \vee (Q \rightarrow R))$.
    2. $\neg(P \rightarrow Q)$. (from (1), by $\neg \vee$-rule)
    3. $\neg(Q \rightarrow R)$. (from (1), by $\neg \vee$-rule)
    4. $P$. (from (2), by $\neg \rightarrow$-rule)
    5. $\neg Q$. (from (2), by $\neg \rightarrow$-rule)
    6. $Q$. (from (3), by $\neg \rightarrow$-rule)
    7. $\neg R$. (from (3), by $\neg \rightarrow$-rule)
    X
    The tableau is closed, as (5) contradicts (6).

    ReplyDelete

Subscribe to: Post Comments (Atom)