Examples

Examples

These are simple arguments and logical theorems (or, in some cases, disproofs). Select an example. To run a sample proof - click on the 'prove' button within an example (this will be at the bottom of the forms); use the browser 'back' to select another example.

Note: A few of the tests are deliberate disproofs, as a check on soundness. These tests are positively proved invalid and are noted as such when they are run.

Tau accepts input in KIF (Knowledge Interchange Format), a first-order notation in ASCII. Documentation for KIF is found here:

For more examples, see a current test suite.