A proposition validation system for verifying the validity of classical propositional statements.
The expected usage is as a command line executable that can take a proposition such as:
$ logic “p and ~p”
Invalid:
Contradiction: found both ‘p’ and ‘~p’
If used on a valid statement, the executable would respond with the valid cases. For example, take the transitivity of the conditional:
$ logic “((p -> q) and (q -> r)) -> (p -> r)”
Valid
Underlying this system is a basic proof-tree mechanism. See analytic tableaux.
- Improve output
- current only valid/invalid, but required information for specific success/fail cases is available -- see Usage