% AILog representation of a meta-interpreter that uses built-in calls and disjunction
% This is the code of Figure 13.11 in Section 13.5.3 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 'prove2.ail'.
% The base-level uses <= for "if" and true for the empty body.
% prove(G) means G is a consequence of the base-level knowledge base
prove(true).
prove((A & B)) <-
prove(A) &
prove(B).
prove((A;B)) <-
prove(A).
prove((A;B)) <-
prove(B).
prove(H) <-
built_in(H) &
call(H).
prove(H) <-
(H <= B) &
prove(B).
% 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 prove:
% ailog: tell le(X,Y) <= X