Learning Resources

If you want to learn more about IDP-Z3 and eco-system, there are a number of places that you could check out.

• IDP-Z3 By Example , an online tutorial designed to teach you the basics of FO(·) and IDP-Z3 through multiple interactive exercises.
• The FO[·] standard , detailing the core language of IDP-Z3.
• The IDP-Z3 docs , a reference overview of everything that’s possible with our engine.
• The cDMN docs , detailing an alternative notation to FO(·).

IDP-Z3 Quick Demo

Let’s build an intelligent application together.

In this section, we will present a concrete problem case and show you how it can be modelled in IDP-Z3. Afterwards, we introduce the Interactive Consultant as a tool for answering questions about the problem domain.

To start, imagine a case as follows:

The case

A local handyman is an expert at hanging objects on walls. Sometimes he uses a nail, sometimes he uses glue, sometimes he uses a screw. Over the years, he has gathered the following knowledge:

• Nails support weights up to 25kg, screws support up to 40kg and glue supports only 15kg.
• Nails and screws require drilling holes in the wall, which cannot be done in tile walls.
• Glue is the easiest to use, a nail takes slightly more effort, and a screw is hardest to use.

With this knowledge, he wants to answer questions such as:

• Which method is easiest for hanging a 20kg weight on a brick wall?
• There is a nail in my wall. How much weight will it support?
• I want to hang a heavy object on my wooden wall, without knowing precisely how heavy it is. Which method will support the most weight?
• Can we hang a 25kg object on a tile wall?
• Where can I hang 20 kg?

How can the handyman leverage this knowledge?

We’ll enter this knowledge in an IDP-Z3 knowledge base and use the Interactive Consultant to obtain answers to these questions.

The Knowledge Base

Below, you can find a formal representation of the knowledge written in FO(·), an extended version of the well-known First Order Logic. This representation is also called a Theory. Note that it consists of two blocks:

• vocabulary block: declares the symbols that describe the problem domain.
• theory block: contains the “laws of the field” written in FO(·) formulas and definitions.

Feel free to skim over the full theory and see if you can understand what it says. If you cannot understand it yet, don’t worry – you do not need to fully understand it to be able to follow the rest of this demo.

vocabulary { 
    type Method ≜ {Nail, Glue, Screw}
    type Wall ≜ {Brick, Wood, Tile}
 
    wall  : () → Wall
    method: () → Method
    hole : () → 𝔹
    weight: () → ℤ
    difficulty : () → ℤ
}
theory {
    weight() > 0.
    method() = Nail  ⇒ weight() ≤ 25.
    method() = Screw ⇒ weight() ≤ 40.
    method() = Glue  ⇒ weight() ≤ 15.

    hole() ⇔ method() = Nail ∨ method() = Screw.
    wall() = Tile ⇒ ¬hole().

    { difficulty() = 1 ← method() = Glue.
    difficulty() = 2 ← method() = Nail.
    difficulty() = 3 ← method() = Screw.}
}

vocabulary {
    type Method := {Nail, Glue, Screw}
    type Wall := {Brick, Wood, Tile}

    wall  : () -> Wall
    method: () -> Method
    hole : () -> Bool
    weight: () -> Int
    difficulty : () -> Int
}
theory {
    weight() > 0.
    method() = Nail  => weight() =< 25.
    method() = Screw => weight() =< 40.
    method() = Glue  => weight() =< 15.

    hole() <=> method() = Nail | method() = Screw.
    wall() = Tile => ~hole().

    {
        difficulty() = 1 <- method() = Glue.
        difficulty() = 2 <- method() = Nail.
        difficulty() = 3 <- method() = Screw.
    }
}

The Interactive Consultant

As mentioned, the Interactive Consultant is a tool that lets you interact with the knowledge in any theory. In short: it allows you to select / deselect value assignments for each symbol in your theory, after which it will automatically derive any consequences for the other symbols. This ensures that you can interactively explore your problem domain, without ever being able to make any mistakes. Additionally, it can also explain why it derived something, and it can also find optimal values. Intrigued? Let’s try it out!

Firstly, let’s open up the above theory in the Interactive Consultant. By clicking on the button below, the IC will open with the theory pre-loaded. To check if the theory is loaded correctly, you can click on “Edit” in the top of the screen to view it. Important to note is that the IC is fully generic: it automatically generates an interface for any theory which you enter!

We will now show you how to use the IC to answer each question of the use case. You’ll have to input some information each time, so it might be easier to open this page and the IC in parallel.

Maintaining the Knowledge Base

Ah, the handyman now has additional knowledge: there is an exception to the rule about tiles, if you have an adequate diamond drillbit. Let’s update the theory accordingly!

• Add “diamond_drill_bit: () → 𝔹” to the vocabulary
• Replace the rule on line 18 by “wall() = Tile ∧ ¬diamond_drill_bit() ⇒ ¬hole().“I
• Click on “Run consultant”

The interface is now updated automatically. Try it out! Can you drill a hole in tile now?

The webIDE

Besides the IC, there are of course other ways to interact with IDP-Z3. For instance, it exposes an API that can be used to reason with any theory. The online IDE allows you to experiment with this:

In the linked example, we perform “model expansion” on our handyman theory. In essence, this will try to find as many possible solutions to the problem as possible. Besides model expansion, there are a plethora of other inferences that can be applied to your knowledge. For more information, see the resources listed at the top of the page.

Real life example

This handyman example is inspired by an IDP-Z3-based tool developed for the Flanders Make Joining and Materials Lab. The following video provides some more context.