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:
the Interactive Consultant, which allow a knowledge expert to enter knowledge about a particular problem domain, and an end user to interactively find solutions for particular problem instances;
a program with a command line interface to compute inferences on a knowledge base;
a web-based Interactive Development Environment (IDE) to create Knowledge bases.
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
-
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
bypython3.9
in the commands below
- Run
poetry install
Run
poetry install --no-dev
if you do not plan to contribute to IDP-Z3 development
- Run
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
the Interactive Consultant at http://127.0.0.1:5000
the webIDE at http://127.0.0.1:5000/IDE
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
the Interactive Consultant at http://127.0.0.1:5000
the webIDE at http://127.0.0.1:5000/IDE
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