% AILog representation of the base-level representation of the electrical example
% This is slightly expanded code of Figure 13.10 in Section 13.5.2 of
% Poole and Mackworth, Artificial Intelligence: foundations of
% computational agents, Cambridge, 2010.
% Copyright (c) David Poole and Alan Mackworth 2009. This program
% is released under GPL, version 3 or later; see http://www.gnu.org/licenses/gpl.html
% To run this in AILog, you should put it in the same directory as AILog and then call
% load 'prove.ail'.
% load 'elect_base.ail'.
% Here "<=" is the object-level "if" and is a meta-level predicate.
% "&" is the object-level conjunction and is a meta-level function symbol.
% lit(L) is true if light L is lit.
lit(L) <=
light(L) &
ok(L) &
live(L).
% live(W) is true if W is live (i.e., current will flow through it if grounded)
live(W) <=
connectedto(W,W1) &
live(W1).
live(outside) <= true.
% light(L) is true if L is a light
light(l1) <= true.
light(l2) <= true.
% connectedto(W0,W1) is true if W0 is connnected to W1 such that current will
% flow from W1 to W0.
connectedto(l1,w0) <= true.
connectedto(w0,w1) <= up(s2) & ok(s2).
connectedto(w0,w2) <= down(s2) & ok(s2).
connectedto(w1,w3) <= up(s1) & ok(s1).
connectedto(w2,w3) <= down(s1) & ok(s1).
connectedto(l2,w4) <= true.
connectedto(w4,w3) <= up(s3) & ok(s3).
connectedto(p1,w3) <= true.
connectedto(w3,w5) <= ok(cb1).
connectedto(p2,w6) <= true.
connectedto(w6,w5) <= ok(cb2).
connectedto(w5,outside) <= ok(outside_connection).
% up(S) is true if switch S is up
% down(S) is true if switch S is down
down(s1) <= true.
up(s2) <= true.
up(s3) <= true.
% ok(G) is true if G is working. Everything is ok:
ok(X) <= true.
% Example Queries:
% ask prove(live(w6)).
% ask prove(live(p1)).
% ask prove(lit(L)).
% ask prove(lit(l2)&live(p1)).
% ask prove(live(L)).