Skip to main content

IDP-Z3 is a reasoning engine for knowledge represented using the FO(.) (aka FO-dot) language.

Project description

idp-engine is a reasoning engine for knowledge represented using the FO(·) language. FO(·) (aka FO-dot) is First Order logic, with various extensions to make it more expressive: types, equality, arithmetic, inductive definitions, aggregates, and intensional objects. The idp-engine uses the Z3 SMT solver as a back-end.

It is developed by the Knowledge Representation group at KU Leuven in Leuven, Belgium, and made available under the GNU LGPL v3 License.

See more information at


idp_engine can be installed from, e.g. using pip:

   pip install idp_engine

Get started

The following code illustrates how to run inferences on a knowledge base.

    from idp_engine import IDP, model_expand
    kb = IDP.parse("path/to/file.idp")
    T, S = kb.get_blocks("T, S")
    for model in model_expand(T,S):

For more information, please read the documentation.


Contributions are welcome! The repository is on GitLab.

Project details

Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

idp_engine-0.11.1.tar.gz (98.3 kB view hashes)

Uploaded Source

Built Distribution

idp_engine-0.11.1-py3-none-any.whl (112.6 kB view hashes)

Uploaded Python 3

Supported by

AWS AWS Cloud computing and Security Sponsor Datadog Datadog Monitoring Fastly Fastly CDN Google Google Download Analytics Microsoft Microsoft PSF Sponsor Pingdom Pingdom Monitoring Sentry Sentry Error logging StatusPage StatusPage Status page