Don't forget to check out the examples.
tl;dr: Write a first-order proposition about blocks, put some blocks in the world, then press "Check World" to see if the proposition holds for the world you've constructed.
You can use the buttons to write a first-order formula. These fill in a text box. After you learn the notation, you can skip the buttons type your formula directly. The formula displays below the box in mathematical notation. The color changes from red to blue when the notation is right.
Colored shapes ("blocks") can be moved onto the grid (the "world") using the mouse.
Press "Check World" to see whether the formula is true or false given in the world.
There must be at least one block in the world.
There are many ways to write operators and connectives, including Latex, Asciimath, and a few extensions of our own.
The connectives are:
| Connective | Input symbols |
|---|---|
| \(\neg\) | \neg not |
| \(\wedge\) | \wedge ^^ and \and |
| \(\vee\) | \vee vv or \or |
| \(\implies\) | \implies -> |
| \(\leftrightarrow\) | \bicond <-> |
| \(\oplus\) | \xor o+ xor |
| \(\forall x\) where \(x\) is a variable | \forall AA |
| \(\exists x\) where \(x\) is a variable | \exists EE |
| \(\T\) aka \(\top\) | \T |
| \(\F\) aka \(\bot\) | \F |