% 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)).