IDP-Z3 Tutorial

Let's build an intelligent application together.

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, but one cannot drill holes in tiles.
Glue is easiest to use, a nail takes slightly more effort, a screw is hardest to use.

With this knowledge, he can 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 ?

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

The knowledge of the handyman can be represented in FO(.) in a text file with two blocks: a "vocabulary" block and a "theory" block. The theory block contains the laws of the field in familiar math notation. (The display block controls, well, the display)

        vocabulary {
    type Method ≜ {Nail, Glue, Screw}
    type Wall ≜ {Brick, Wood, Tile}
    type Difficulty ≜ {1..3}

    wall  : () → Wall
    method: () → Method
    hole : () → 𝔹
    weight: () → ℤ
    difficulty : () → 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.}
}
display {
    view() = expanded.
}

More about FO(.)

The Interactive Consultant

To configure the Interactive Consultant for this knowledge base, follow these steps:

Open the Interactive Consultant. A default application is displayed.
Select "Edit" in the menu to open the knowledge base of the default application.
Copy the knowledge base above, and paste it to replace the default knowledge base in the editor.
Click "Run Consultant"

(or simply click here ).

Congratulations ! You have now created an intelligent application !
You can now use it to enter what you know (or want) in your particular situation: the display will be immediately updated with the consequences of your entry.

Which method is easiest for hanging a 20kg weight on a brick wall?

Set the "weight" to 20: you'll see that you cannot use glue.
Click on the downwards arrow next to "difficulty": the tool recommends "nails" as the easiest method, and says you'll need to drill a hole.
Click on the checkmark next to "hole" to obtain an explanation

There is a nail in my wall. How much weight will it support?

Choose "Reset / Full" in the menu to consider a new situation.
Select the "nail" method.
Click the upwards arrow next to "weight": you'll see that the maximum weight is 25 kg.

Which method will support the most weight on a wooden wall?

Choose "Reset / Full".
Select the "Wood" wall in the dropdown.
Click the upwards arrow next to "weight": you'll see that the maximum weight is 40 kg, for the "Screw" method.

Can we hang a 25kg object on a tile wall?

Choose "Reset / Full".
Set the weight to 25kg: "Tile" wall is not possible.
Click on the cross next to "Tile" to obtain an explanation.

Maintaining the Knowledge Base

Ah, the handyman tells you that there is an exception to the rule about tiles: it is possible to drill a hole if you have the adequate diamond drillbit. Let's update the Knowledge Base accordingly.

Add "diamond_drill_bit: () → 𝔹" to the vocabulary
Replace the rule "wall() = Tile ⇒ ¬hole()." by "wall() = Tile ∧ ¬diamond_drill_bit() ⇒ ¬hole()."
Click "Run consultant": the form is updated.

The web IDE

The IDP-Z3 reasoning engine exposes an API that can be used to reason with the knowledge. The online IDE allows you to experiment with it. Follow these steps:

Choose "View / View in IDE" to open the online IDE. A warning message warns you that a "main" block will be added to the knowledge base.
Click "Ok" to dismiss the warning. The online IDE appears, with the knowledge base on the left, and the output pane on the right. The "main" block has a command to show the possible state of affairs, according to the theory.
Choose "Run" in the menu. The output pane shows 10 possible states of affairs.

Where can I hang 20 kg ?

Add the following sentence after line 11: "weight() = 20."
Choose "Run" in the menu. The output pane lists 4 possibilities.

To learn more:

IDP-Z3 by Example IDP-Z3 Reference

This example is inspired by a system developed for the Flanders Make Joining and Materials Lab. The following video provides some more context.