This is a companion repository to Tarski.

Latest is 1.0.1 (Apr 09, 2026) staying in sync with the main repository.

You will need a JVM, and Scala 3. This should give you everything you need.

An easier way is to install Scala-cli which can automatically install a JVM for you.

To work through the examples, install git, clone this repository with

git clone https://github.com/spamegg1/tarski-examples

then open the folder in your IDE (Visual Studio Code with Metals extension, or IntelliJ with Scala plugin).

Each example has a README with instructions. In some examples, you might have to write some formulas first, before executing.

To interact, execute the @main methods with names like run02a etc.

If the window is too small or too big, you can pass an optional parameter to resize it:

// Make the window smaller, shrink it to 80% size
@main
def run01a = runWorld(LeibnizWorld, RebusSentences, 0.8)

There are 79 examples in total. The first 28 are for Propositional Logic and the last 51 are for Quantifier Logic, getting more difficult as you progress.

There are two kinds of equality used in the examples.

Reference equality a.k.a "identity" (or "identical" when used as an adjective) means that two names a, b are referring to the same block, and is implemented using a = b. So in this case a and b have the same location (row and column) on the board.

Value equality a.k.a "equality" (or "equal" when used as an adjective) means that two blocks a, b are equal in size, shape and tone, and is implemented using Eq(a, b).