% AILog representation of a meta-interpreter that builds a proof tree. % This proof tree is what used to implement "how" (but this is not implemented here). % This is the code of Figure 13.13 in Section 13.5.5 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 'hprove.ail'. % The base-level uses <= for "if" and true for the empty body. % hprove(G,T) means G is a consequence of the base-level knowledge % base, and T is a representation of the corresponding proof hprove(true,true). hprove((A & B),(L&R)) <- hprove(A,L) & hprove(B,R). hprove(H,if(H,built_in)) <- built_in(H) & call(H). hprove(H,if(H,T)) <- (H <= B) & hprove(B,T). % built_in(G) is true if G is to be proved in the underlying ailog system built_in(V is E). built_in(X < Y). built_in(X > Y). % Here is an example is the use of hprove: % tell le(X,Y) <= X