IDP-Z3, a reasoning engine for FO(.)

FOSDEM 2023

An important sign of intelligence is the capacity to apply a body of declarative knowledge to a particular situation in order to, e.g., derive new knowledge, to determine relevant questions or to provide explanations. IDP-Z3 is a reasoning engine that displays such intelligence: the knowledge is represented in the declarative language FO(.), aka FO-dot, and, based on that knowledge, IDP-Z3 can perform a variety of reasoning tasks under the control of a host language, Python. This re-use of knowledge dramatically reduces software development time. FO(.) is an expressive, yet very readable language that extends first order logic. We present IDP-Z3, and how we used it to build a generic user interface, called the Interactive Consultant, that helps end-users make the right decision fast, within a particular problem domain.

FO(.) (aka FO-dot) is the Knowledge Representation language used by the IDP-Z3 reasoning engine.

FO(.) was introduced by Prof. Denecker (KU Leuven). It is based on first-order logic (FOL) for its constructs (i.e., logic connectives and quantification). FO(.) extends FOL with a few language constructs to express complex information such as non-inductive, inductive and recursive definitions, and aggregates.

An FO(.) Knowledge Base consists of a vocabulary and a "theory". The vocabulary describes the domain-specific symbols that are used in the theory. A theory is a collection of assertions about possible state of affairs. There are three classes of assertions: constraints, definitions and enumerations. States of affairs are represented by structures, that contains the values of the symbols of the vocabulary. A structure that is possible according to the theory is called a model.

A Knowledge Base (KB) written in FO(.) cannot be run: it is just a "bag of information" formally describing models in a problem domain. This is a consequence of the FO(.) design goal to be task-agnostic. A corollary is that such a KB does not distinguish inputs from outputs, and allows reasoning in any direction.

A key advantage of the model-theoretic semantics is that it allows reasoning with incomplete knowledge of the state of affairs. This knowledge is encoded in a partial structure. When not much is known, many states of affairs are possible, and the theory has many models representing them. As more information is obtained, the set of models is reduced. This reduced set of models can be used to perform various forms of reasoning, e.g., to derive the consequences of what is known, or to find the model that maximizes a utility function.

As a very simple example, consider the voting law that states: "You have to vote in an election if you are at least 18 years old at election time (otherwise you can not)". The formula in FO(.) is:

vote() <=> 18 =< age().

If the age is known, the obligation to vote can be inferred; if the obligation to vote is known to be true instead, the age is known to be 18 or more, in any model. Furthermore, one can also find a lower bound of the age of a person, as soon as their obligation to vote is known.

IDP-Z3 is a reasoning engine that can perform a variety of reasoning tasks on knowledge bases in the FO(.) language. The following generic computations are supported by IDP-Z3:

Model checking: Verifies that a theory is satisfiable given a structure, i.e., that it has at least one model.
Model expansion: Takes a theory T and a partial structure S, and computes a model of T that expands S, if one exists.
Propagation: Takes a theory T and a partial structure S, and computes all their logical consequences, i.e., all the ground literals that are true in every model expansion of T and S.
Explanation: Takes a theory T, a partial structure S and a literal L obtained by propagation, and computes an explanation for L in the form of a minimal set of axioms in $T \cup S \cup {\lnot L}$ that is inconsistent.
Optimisation: Takes a theory T, a partial structure S and a term, and computes the minimal value of the term in the set of all model expansions of T and S.
Relevance: Takes a theory T and a partial structure S, and determines the atoms that are irrelevant (or ``do-not-care'') in the sense that, if one of their value were changed in any model M of T expanding S, the resulting M' structure would still be a model of T.

IDP-Z3 can be run at the command line, or integrated in a Python application as a Python package downloadable from pypi (https://pypi.org/project/idp-engine/). Computations can also be run online via a webIDE (https://interactive-consultant.idp-z3.be/IDE). It is open source (https://gitlab.com/krr/IDP-Z3) under the LGPL 3 license.

IDP-Z3 comes with a demo web application, called the Interactive Consultant, that helps users make decision in accordance with an FO(.) knowledge base, using the reasoning abilities of IDP-Z3.

It is generic in the sense that it can be reconfigured by simply changing the FO(.) knowledge base. The user interface is automatically generated based on the vocabulary of the knowledge base: this helps reduce the cost of developing applications significantly. It is available online (https://interactive-consultant.idp-z3.be/).

The Interactive Consultant (IC) allows the user to enter data in any order.
The IC enables a safe exploration of the decision search space, without the possibility of making decisions leading to dead ends. This is achieved by continuously computing the consequences of the data theory, using propagation. If the user is unsure why the IC propagated a specific choice, they can ask for an explanation. Additionally, while the user fills in what they know, the interface determines which parameters remain relevant, avoiding unnecessary work for the user. After having input all values that they deem necessary, the user can ask the IC to show the optimal decision according to what is known, using optimization.

Speakers: Pierre Carbonnelle