Introduction

IDP-Z3 is a software collection implementing the Knowledge Base paradigm using the FO[·] language. FO[·] (aka FO-dot) is First Order logic, extended with definitions, types, arithmetic, aggregates and intensional objects. In the Knowledge Base paradigm, the knowledge about a particular problem domain is encoded using a declarative language, and later used to solve particular problems by applying the appropriate type of reasoning, or “inference”. The inferences include:

  • model checking: does a particular solution satisfy the laws in the knowledge base ?

  • model search: extend a partial solution into a full solution

  • model propagation: find the facts that are common to all solutions that extend a partial one

The IDP-Z3 engine enables the creation of these solutions:

Warning

You may want to verify that you are seeing the documentation relevant for the version of IDP-Z3 you are using. On readthedocs, you can see the version under the title (top left corner), and you can change it using the listbox at the bottom left corner.

Installation using poetry

Poetry is a package manager for python.

  • Install python3 on your machine

  • Install poetry

    • after that, logout and login if requested, to update $PATH

  • Use git to clone https://gitlab.com/krr/IDP-Z3 to a directory on your machine

  • Open a terminal in that directory

  • If you have several versions of python3, and want to run on a particular one, e.g., 3.9:

    • run poetry env use 3.9

    • replace python3 by python3.9 in the commands below

  • Run poetry install
    • Run poetry install --no-dev if you do not plan to contribute to IDP-Z3 development

To launch the Interactive Consultant web server:

  • open a terminal in that directory and run poetry run python3 main.py

After that, you can open

Installation using pip

IDP-Z3 can be installed using the python package ecosystem.

  • install python 3, with pip3, making sure that python3 is in the PATH.

  • use git to clone https://gitlab.com/krr/IDP-Z3 to a directory on your machine

  • (For Linux and MacOS) open a terminal in that directory and run the following commands.

python3 -m venv .
source bin/activate
python3 -m pip install -r requirements.txt
  • (For Windows) open a terminal in that directory and run the following commands.

python3 -m venv .
.\Scripts\activate
python3 -m pip install -r requirements.txt

To launch the web server on Linux/MacOS, run

source bin/activate
python3 main.py

On Windows, the commands are:

.\Scripts\activate
python3 main.py

After that, you can open

Installation of idp_engine module

The idp_engine module is available for installation through the official Python package repository. This comes with a command line program, idp_engine that functions as described in Command Line Interface.

To install the module via poetry, the following commands can be used to add the module, and then install it.

poetry add idp_engine
poetry install

Installing the module via pip can be done as such:

pip3 install idp_engine