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.
}
      

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:

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