% prove1.pl

% simple meta-interpreter for prolog,
% written in prolog of course
:- [demos, star,elec].

% new main demo driver- demof
demof :- demos(prove1).

% demos hooks into demo1
demo1 :- nl, write('prolog: '),
	prolog(live(X)),
	format(' ~w',X).
demo1 :- nl, write('prove : '),
	 prove(live(X)),
	 format(' ~w',X).
demo1 :- nl, write('delta :  '),
     1000*prolog(live(_))/prove(live(_)).

% just call raw prolog
prolog(X) :- X.

% the "clause/2" predicate lets prolog
% access the definitions of asserted
% clauses. clause(head,body) ==> looks
% it up in the current rule
% clause(fact,X) ==> X = true

% cuts are needed cause the last clause
% is a "do everthing that is not the
% above". bad cuts, bad.

% base case
prove(true)  :- !.

% negation
prove(\+ X)  :- !,
	\+ prove(X).

% disjunction
% warning- note the brackets
% around the disjunction
prove((A;B)) :- !,
	(prove(A)
        ; prove(B)).

% conjunction
prove((A,B)) :- !,
	prove(A),
	prove(B).

prove(A) :-
	clause(A,B),
	prove(B).