IDP-Z3 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, arithmetic, inductive definitions, aggregates, and intensional objects.
Once the knowledge of a problem domain is encoded in FO(.), the engine can perform a variety of reasoning tasks: find relevant questions to solve a particular problem, derive consequences from new information, explain how it derived these consequences, find a solution that minimizes a cost function, …
IDP-Z3 is developed by the Knowledge Representation group at KU Leuven in Leuven, Belgium, and made available under the GNU LGPL v3 License. It uses the Microsoft Z3 solver as back-end to perform the reasoning tasks. (The previous version of the reasoning engine, IDP3, used minisat)
The IDP-Z3 reasoning engine is currently deployed in the following open-source projects:
the Interactive Consultant, a tool enabling experts to encode their knowledge of a problem domain, and to automatically create an interactive web tool that helps end users find solutions for specific problems in that domain.
DMN-IDP, a user-friendly tool which combines the readability of the Decision Model and Notation (DMN) standard with the power of the IDP system through an interactive interface.
IDP-Z3 has also been used in private projects by Saint-Gobain, Flanders Make, and a partner in the financial sector, among others. These projects use a data-poor, knowledge-rich approach to Artificial Intelligence to leverage the knowledge of the experts in their fields.
Our partners particularly appreciate the ease of encoding this knowledge in FO(.): its expressivity removes a long-standing barrier in the use of Knowledge Base systems.