EXPRWEB

What this is:

Exprweb is a port of my exprgraph propositional tableaux prover and my exprtest natural deduction prover to the web.

Grammar:

• All formulas except negations and single variables are parenthesized.
• # or @ being a single upper case alphabetical character is well formed.
• # or @ may also be one of the compound expressions listed below.
• (#v@) is a well formed or expression.
• (#&@) is a well formed and expression.
• (#->@) is a well formed conditional expression.
• ~@ is a well formed not expression.
• No other expression is well formed.

Example:

~((AvB)&~~(~C->~D)) is a well formed formula

Input:

Enter a list of semicolon separated well formed formulas as premises and a single well formed formula as a conclusion.

Exprtest Inference Rules:

These are modified from Harry Genslers intro to logic book.

• {(AvB), ~A |- B} for v's}
• {(A&B) |- A, B} for &'s}
• {(A->B), A |- B} for ->'s (modus ponens)}
• {(A->B), ~B |- ~A} for ->'s (modus tollens)}
• {~~A |- A} double negation}{
• {~(AvB) |- ~A, ~B} negated v's}
• {~(A&B), A |- ~B} negated &'s}
• {~(A->B) |- A, ~B} negated ->'s}

Exprgraph Inference Rules:

These are modified from Graham Priests introductory book on non-classical logic.

• (A&B), conjunctions extend all leaves with A and B individually.
• (AvB), disjunctions extend each leaf with a fork, one side containing A the other containing B.
• (A->B), conditionals are interpreted as the material conditional (~AvB) and the disjunctive rule above is applied to this formula.
• ~(AvB), negated disjunctions are interpreted based on demorgans law as (~A&~B) and the conjunctive rule above is applied to this formula.
• ~(A&B), negated conjunctions are interpreted based on demorgans law as (~Av~B) and the disjunctive rule above is applied to this formula.
• ~(A->B), negated conditionals are interpreted based on demorgans law on the material conditional as (A&~B) and the conjunctive rule above is applied to this formula.
• ~~A, double negations extend each leaf with the original formula, for example ~~A extends the tree with A.

Note: The above tableaux rules can be condensed down to three via various uniform notations. The program logic for this particular program did not work out exactly like that but generally I think of three kinds of operations that are performed by exprgraph: disjunctive/splits, conjunctive/extensions and double negation based extensions. Pictorial representations of the above rules can be found here under propositional logic.

Further Info: