Drag and drop the blocks to create a world. Enter a corresponding first order logic formula:

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 symbol
\(\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`

Examples

\forall x (Red(x) \implies \forall y (Below(x,y)))
\exists x (Red(x) \wedge \forall y (Below(x,y)))

Common errors

Syntax errors will print ugly messages that usually do a good job of locating the error, except sometimes for missing right parentheses.
Everything is case-sensitive. Note that all predicates begin with a capital letter (e.g., "Blue" and "LeftOf"). Anything other than the predicates listed above will produce an "undefined error" message.
Free variables generate "undefined variable" errors.

CS 103 Blocks World

Examples

Common errors