Question 2

Question 2

In this example, constants p1, p2 and p3 denote cold water pipes. p1 is the pipe coming in from the main water supply. Constants p4 and p5 represent hot water pipes (coming out from the hot water system). Constants t1, t2 t3, t4 and t5 denote taps and d1, d2 and d3 denote drainage pipes. The constants shower denotes a shower, bath denotes a bath, sink denotes a sink, hws denotes a hot water system, and floor denotes the floor. The diagram below is intended to give the denotation for the constant symbols.

Suppose we have as predicate symbols:

• pressurised, where pressurised(P) is true if pipe P has mains pressure in it. p1 is always pressurized. Other pipes are pressurized if they are connected to a pressurized pipe through an open tap.
• on, where on(T) is true if tap T is on.
• off, where off(T) is true if tap T is off.
• wet, where wet(B) is true if B is wet.
• flow, where flow(P) is true if water is flowing through P.
• plugged, where plugged(S) is true if S is either a sink or a bath and has the plug in.
• unplugged, where unplugged(S) is true if S is either a sink or a bath and doesn't have the plug in.

The file plumbingbuggy.pl contains a CILog axiomatization for the case where tap t1 is on, t2 is on, t3 is off, t4 is off, t5 is off, and t6 is on. There is a plug in the sink, but not in the bath. (This has been formatted to be unreadable, but you don't need to be able to read the program, or know how it is implemented, to be able to debug it.)

Unfortunately there is a bug in the program. We know this because we can prove that the floor is wet, even though it isn't wet in the intended interpretation. Using CILog, your goal is to find a clause that is false in the intended interpretation, using just the intended interpretation of the symbols.

You need to hand in a trace of the CILog session, and show clearly which is the buggy rule.

• Solution

Question 2