Tarski UdeS Manual

Keyboard Shortcuts

Ctrl+Shift+F Format code area
Ctrl + Mouse Scroll Resize code area text size
Ctrl+R Eval all formulas

Logical connectives and quantifiers:

& conjunction
or disjunction
=> implication
<=> equivalence
not negation
!x.(formula) for all (where x is any single character variable)
#x.(formula) there exists (where x is any single character variable)

Predicates:

Triangle(x) x is a triangle
Square(x) x is a square
Pentagon(x) x is a pentagon
Small(x) x is small
Medium(x) x is medium
Large(x) x is large
Smaller(x,y) x is smaller than y
SameSize(x,y) x and y have the same size
SameCol(x,y) x and y are in the same column
SameRow(x,y) x and y are in the same row
LeftOf(x,y) the column of x is on the left of the column of y
Between(x,y,z) x is between y and z on a row, column or diagonal

Equality:

x = y x is equal to y
x /= y x is different from y

All Variables: lowercase letters [a-z]

Single line comments '//'

Multiline comments '/* (...) */'

For MacOs users on Catalina:

You will need to allow the integrated java executable (packaged with this image) to run with the following command: xattr -d com.apple.quarantine /path/to/your/tarski/folder/tarski-udes-x64-mac/bin/java