Learn IDP-Z3 #

IDP-Z3 is a logical reasoning engine for FO(·), an extension of classical first order logic. It allows us to express knowledge of a problem domain declaratively, and to then execute many built-in inference tasks to put the knowledge to use and solve problems.

This website contains a tutorial for learning how to work with IDP-Z3 and FO(·). Its main philosophy is to “learn by doing”, and as such is centered around interactive examples throughout the tutorial. You should feel encouraged to try out all these examples yourself – after all, that is the best way to learn.

The tutorial is split up in multiple sections:

• Introduction
• Defining the Situations
• Properties of Situations