1:- if(( ( \+ ((current_prolog_flag(logicmoo_include,Call),Call))) )).    2:- module(mpred_pttp_unused,[]).    3:- endif.    4
    5%%% Adam Farquhar 9/1/95
    6%%%
    7%%% An interpreted model elimination theorem prover.
    8%%%
    9%%% I use iterative deepening with (1) a filter so that goals found on
   10%%% previous iterations are not returned, (2) a test so that if no
   11%%% paths are pruned due to the depth cutoff, no further deepening
   12%%% will occur, and (3) a method to determine a minimum depth bound
   13%%% increment that might result in a new answer being found.
   14%%%
   15%%% Unification does NOT include an occurs check.  This is because I
   16%%% want to work with a logic that allows for infinite terms.
   17%%%
   18
   19%%% USAGE
   20/***
   21clear
   22  - clear out database and reset any flags.
   23show 
   24   - show the internal clauses.
   25pttp_prove(Goal) 
   26pttp_prove(Goal,InitialBound)
   27pttp_prove(Goal,InitialBound,Max)
   28  - try to pttp_prove the full FOL Goal, which may be of the form
   29    Term^Goal, which will cause the variables in Term to be bound.
   30    pttp_prove constructs a clause query(Term) :- Goal and then tries to
   31    pttp_prove query(Term).
   32prove_goal(Goal)
   33prove_goal(Goal,InitialBound)
   34prove_goal(Goal,InitialBound,Max)
   35  - Use iterative deepening to pttp_prove Goal within Max starting with a
   36    bound of InitialBound. Goal needs to be an atomic formula.
   37prove_goal_bounded(Goal,Ancestors,InitialBound,-Remaining)
   38prove_goal_bounded(+Goal,Ancestors,+Bound,-Remaining)
   39  - Try to pttp_prove Goal within Bound.
   40rule(Head,Body,Cost)
   41  - Clauses are represented with the predicate rule/3.  Calls to
   42    system predicates may be done by asserting rule/3.  E.g., if you
   43    want to allow for append/3 to be accessed, all you need to do is
   44    to assert: 
   45       rule(append(X,Y,Z),[],1) :- append(X,Y,Z).
   46    where [] is the empty body and 1 is the cost of execution.
   47
   48SYNTAX
   49  all(X,some(Y,loves(X,Y))).
   50  a <=> b.
   51  a <= b and c or d.
   52  b and c or d => a.
   53  ~(a and b) <=> ~a or ~b.
   54
   55***/
   56
   57%%% BUGS
   58%%% 
   59%%% 9/12/95 No known bugs.
   60%%%
   61
   62%%% CHANGES
   63%%% 9/12/95
   64%%% * Eliminated builtin.  The same effect can be achieved by using
   65%%% rule/3. Improved id;  Added max, tally/3.  Simplified and rewrote
   66%%% contrapositives.  Eliminated unused code.  Tried using ord... for
   67%%% ancestor list, but removed it because it slowed things down on the
   68%%% current examples.  On hpp-ss10d-3, e5(100) takes 1 sec,
   69%%% chang_lee_example2 takes 8 sec.
   70%%%
   71
   72%%% TODO
   73%%%
   74%%% - Figure out how to write apply, holds, inverse, function.
   75%%%
   76%%% - The clausal form converter seems to reverse the order of
   77%%% predicates occasionaly.  This can be trouble with builtins like
   78%%% is/2, which require certain vars to be bound.
   79%%%
   80%%% - pttp_prove needs a better interface for collecting bindings.
   81%%% E.g. if we query some(X,p(X)), then the X gets renamed when
   82%%% converting to clausal form, so we don't see the bindings.
   83%%%
   84%%% - Contrapositives should be careful with builtins.  We should
   85%%% probably not include them.  We also need to be careful with
   86%%% ordering in clause formation (see bugs).
   87%%%
   88%%% - See what the effect of indexing the ancestor list would be.  We
   89%%% used to have two lists (as did Stickel) -- one for postive and one
   90%%% for negative ancestors.  The main reason for this was that Stickel
   91%%% used the functor not_xxx rather than ~(xxx) to represent negation.
   92%%% This made run-time computation of the negation more expensive.
   93%%% + I tried using ord_add_element and ord_identical_member for the
   94%%% ancestor list.  This slowed things down on the example problems,
   95%%% none of which have very deep ancestor lists (11 for chang/lee2).
   96%%% Perhaps a good binary tree would be worth the effort.
   97%%%
   98%%% - Should the rules be passed as an argument rather than indexed in
   99%%% the database?  If so, be careful about variable bindings!  This
  100%%% would probably be faster for simple examples.  For larger
  101%%% problems, it would depend on the quality of the indexing
  102%%% mechanism.  Since we currently lose the principle functor index
  103%%% (they are all 'rule') it might still be a win.
  104%%%
  105%%% - Collect Proof
  106%%%
  107
  108%%% ISSUES
  109%%%
  110%%% - Should I use member or identical_member when checking for an
  111%%% ancestor?  Should the test backtrack to look at more ancestors? (I
  112%%% don't think so).  Should I use subsumes_chk?
  113%%%

  120:- use_module(clause).  121:- use_module(library(basics)).  122:- use_module(library(lists)).  123:- was_dynamic rule/3.
  124
  125%%% Model Elimination Theorem Prover
  126%%%
  127
  128clear :- abolish(rule/3),
  129	assert_list(
  130	[(rule(apply(X,Y),[],1) :- apply(X,Y)),
  131	(rule(X is Y,[],1) :- X is Y)
  132    ]).
  133
  134show :- listing(rule/3).
  135
  136axioms([]).
  137axioms([H|T]) :-
  138	axiom(H),
  139	axioms(T).
  140
  141axiom(Fol) :-
  142	fol_rules(Fol,Clauses),
  143	assert_list(Clauses).
  144
  145%%% pttp_prove takes an arbitrary FOL statement and tries to pttp_prove it.
  146%%% The Sentence may be a FOL sentence in which case only success/failure
  147%%% is returned, or it can be a term Vars^Sentence, which will cause
  148%%% Vars to have the bindings from the successful proofs.
  149
  150pttp_prove(Sentence) :- pttp_prove(Sentence,5).
  151pttp_prove(Sentence,InitialBound) :- pttp_prove(Sentence,InitialBound,100).
  152
  153pttp_prove(Sentence0,InitialBound,Max) :-
  154	(Sentence0 = Vars^Sentence
  155    ->
  156	Query = query(Vars)
  157    ;
  158	Query = query, Sentence = Sentence0),
  159	retract_query,
  160	axiom(Sentence => Query),
  161	prove_goal(Query,InitialBound,Max).
  162
  163retract_query :-
  164	member(Q,[query,~query,query(_),~query(_)]),
  165	retractall(rule(Q,_,_)),
  166	clause(rule(A,B,C),true),
  167	member(Q,B),
  168	retract(rule(A,B,C)),
  169	fail.
  170retract_query.
  171
  172
  173prove_goal(Goal) :- prove_goal(Goal,5,100).
  174prove_goal(Goal,InitialBound) :- prove_goal(Goal,InitialBound,100).
  175
  176prove_goal(Goal,InitialBound,Max) :-
  177	id(prove_goal_bounded(Goal,[]),InitialBound,Max).
  178
  179prove_goal_bounded(Goal,Anc,_B,_B) :-

  181	

  182	identical_member(Goal, Anc),
  183	!,
  184	fail

  184.
  185prove_goal_bounded(Goal,Anc,B0,B) :-

  187	

  188	negate(Goal,Negated),
  189	identical_member(Negated, Anc),
  190	tally(1,B0,B)

  190.
  191prove_goal_bounded(Goal,Anc,B0,B) :-
  192	rule(Goal,Body,MinProofCost),
  193	tally(MinProofCost,B0,B1),
  194	prove_body(Body,[Goal|Anc],B1,B).
  195
  196prove_body([],_,B,B).
  197prove_body([Goal|Goals],Anc,B0,B) :-
  198	prove_goal_bounded(Goal,Anc,B0,B1),
  199	prove_body(Goals,Anc,B1,B).
  200
  201%%% Convert to Clausal Form and add Contrapositives
  202%%%
  203%%% clausal_form(Fol,Clauses) translates between FOL and Clausal form.
  204%%% Each Clause is a term clause(PosAtoms,NegAtoms).
  205%%% We use a "rule" form in which everything looks like a horn clause.
  206
  207fol_rules(Fol,Rules) :-
  208	clausal_form(Fol,Clauses),
  209	clausal_to_rules(Clauses,Rules).
  210	
  211clausal_to_rules([],[]) :- !.
  212clausal_to_rules([Clause|Clauses],Rules) :-
  213	contrapositives(Clause,Rules0),
  214	clausal_to_rules(Clauses,Rules1),
  215	append(Rules0,Rules1,Rules).
  216	
  217contrapositives(clause(Head,Body),C) :-
  218	negate_list(Head,Not_Head),
  219	append(Not_Head,Body,Atoms),
  220	contras(Atoms,Atoms,C).
  221
  222contras([],_,[]).
  223contras([H|T],Body,[Head_Rule|Tail_Rules]) :-
  224	negate(H,Not_H),
  225	delete(Body,H,ThisBody),
  226	length(Body,Cost),
  227	Head_Rule = rule(Not_H,ThisBody,Cost),
  228	contras(T,Body,Tail_Rules).
  229
  230%%% ITERATIVE DEEPENING
  231%%%
  232%% The idea for this is From O'Keefe pg66.  The iterative deepening
  233%% driver (1) only returns a particular solution/tree one time, and
  234%% (2) increments the depth bound the minimum amount believed
  235%% necessary to find a new solution (using the estimated cost provided
  236%% to tally).  The tally/3 predicate should be called by the Goal
  237%% where appropriate.
  238
  239id(Goal,Bound,Max) :- id(Goal,0,Bound,Max).
  240
  241id(Goal,PrevBound,Bound,Max) :-
  242	Bound =< Max,
  243	flag(depth_cutoff,0),
  244   % the * is not a typo
  245	apply*(Goal,[Bound,Remaining]),
  246	Remaining < Bound - PrevBound.
  247id(Goal,_,Bound,Max) :-
  248	flag(depth_cutoff,Increment),
  249	Increment > 0,
  250	Bound1 is Bound + Increment,
  251	Bound1 =< Max,
  252	%%format('~Nid: Increasing bound to: ~p.~n',[Bound1]),
  253	id(Goal,Bound,Bound1,Max).
  254
  255tally(N,B0,B) :-
  256	(B0 >= N				% or > ?
  257    ->
  258	B is B0 - 1
  259    ;
  260	D is N - B0 + 1,
  261	flag(depth_cutoff,C),
  262	(C = 0 ; C > D),
  263	flag(depth_cutoff,D),
  264	!,
  265	fail
  266    ).
  267
  268%%% General Utilities
  269
  270timed(Goal) :-
  271	statistics(runtime,[T0,_]),
  272	call(Goal),
  273	statistics(runtime,[T1,_]),
  274	Secs is (T1 - T0) / 1000.0,
  275	format('~nExecution took ~p seconds.~n',[Secs]).
  276
  277% the * is not a typo
  278apply*(Goal,MoreArgs) :-
  279	Goal =.. List0,
  280	append(List0,MoreArgs,List),
  281	NewGoal =.. List,
  282	NewGoal.
  283
  284apply(Rel,Args) :-
  285	Goal =.. [Rel|Args],
  286	Goal.
  287
  288assert_list([]).
  289assert_list([H|T]) :- assertz(H),assert_list(T).
  290
  291%ord_identical_member([H|T],X) :-
  292%	compare(Order,X,H),
  293%	ord_identical_member(Order,H,T,X).
  294%ord_identical_member(<,_H,_T,_X) :- !, fail.
  295%ord_identical_member(=,_,_,_).
  296%ord_identical_member(>,_H,T,X) :-
  297%	ord_identical_member(T,X).	
  298
  299identical_member(X,[H|T]) :-
  300	X == H
  301    ->
  302	true
  303    ;
  304	identical_member(X,T).
  305
  306%%% Global flags.  There is probably a library/builtin for this.
  307
  308flag(Flag,Val) :-
  309	var(Val)
  310    ->
  311	global(Flag,Val)
  312    ;
  313	(retractall(global(Flag,_)),
  314	assert(global(Flag,Val))).
  315
  316%%% Logic Utilities
  317
  318negate_list([],[]).
  319negate_list([H|T],[Not_H|Not_T]) :-
  320	negate(H,Not_H),
  321	negate_list(T,Not_T).
  322
  323negate(~(G),G) :- !.
  324negate(G,~(G)).
  325
  326
  327%%% Examples
  328
  329e :- e1,e2,e3,e4,e5,e6,e7,e8,e9,
  330	chang_lee_example1, chang_lee_example2.
  331
  332e1 :-
  333	clear,
  334	axiom((a or b) and ~(a)),
  335	prove_goal(b),
  336	\+ prove_goal(a),
  337	pttp_prove(a or b).
  338
  339e2 :- clear,
  340	axioms(
  341	[rev([],[]),
  342	(rev([X|Xs],Zs) <= rev(Xs,Ys) and append(Ys,[X],Zs)),
  343	append([],Xs,Xs),
  344	(append([X|Xs],Ys,[X|Zs]) <= append(Xs,Ys,Zs))
  345    ]),
  346	pttp_prove(rev([a,b,c],[c,b,a])),
  347	\+ pttp_prove(rev([a,b,c],[c,b,a,z])),
  348	e2(30,497).
  349
  350%nrev([],[]).
  351%nrev([X|Xs],Zs) :- nrev(Xs,Ys),appn(Ys,[X],Zs).
  352%appn([],Xs,Xs).
  353%appn([X|Xs],Ys,[X|Zs]) :- appn(Xs,Ys,Zs).

  368e2(N,B) :-
  369	length(X,N),
  370	numbervars(X,0,_),
  371	timed(prove_goal(rev(X,Y),B,100000)),
  372	reverse(X,Y).

  375e3 :-
  376	clear,
  377	assertz(rule(len([],0),[],0)),
  378	assertz(rule(len([_A|B],N),[len(B,N1),N is N1 + 1],2)),
  379	pttp_prove(X^len([a,b],X)),
  380	X == 2.
  381
  382e4 :- 
  383	clear,
  384	axioms(
  385	[q(X) => p(X),
  386	q(2),
  387	q(1)]),
  388	bagof(X,pttp_prove(X^p(X)),L),
  389	(L = [1,2] ; L = [2,1]).
  390
  391e5_1(0).
  392e5_1(N) :- N > 0, axiom(p(N)),N1 is N-1, e5_1(N1).

  401e5 :- e5(5).
  402e5(N) :-
  403    clear, e5_1(N),
  404    axiom(q(X) <= p(X)),
  405    axiom(r(X,Y) <= p(X) and q(Y)),
  406    %%bagof(r(X,Y),pttp_prove([X,Y]^r(X,Y)),L),
  407    bagof(r(X,Y),prove_goal(r(X,Y)),L),
  408    length(L,Len),
  409    Len =:= N*N.
  410
  411e6 :- clear,
  412	axioms(
  413	[p(X) <= apply(format,['APPLY: ~p~n',[X]]) and q(X),
  414	q(1),
  415	q(2)]),
  416	bagof(X,pttp_prove(X^p(X)),L),
  417	format('Should have done APPLY on ~p.~n',[L]).
  418
  419e7 :- clear,
  420	axiom(a or b or c),
  421	axiom(~c),
  422	pttp_prove(a or b),
  423	\+ pttp_prove(a or c).
  424
  425e8 :- clear,
  426	axiom(a or b or c),
  427	pttp_prove(a or b or c),
  428	\+ pttp_prove(a or b),
  429	\+ pttp_prove(b or c),
  430	\+ pttp_prove(a or c).
  431
  432e9 :- clear,
  433	pttp_prove(~(a and b) <=> ~a or ~b).
  434
  435e10 :- clear,
  436	axiom(p(X) or q(X) <= r(X)),
  437	axiom(r(a) and r(b)),
  438	pttp_prove(X^(p(X) or q(X))),
  439	\+ pttp_prove(p(a)),
  440	\+ pttp_prove(p(b)),
  441	\+ pttp_prove(q(a)),
  442	\+ pttp_prove(q(b)),
  443	\+ pttp_prove(p(a) or q(b)),
  444	pttp_prove(p(a) or q(a)),
  445	pttp_prove(p(b) or q(b)).
  446	
  447chang_lee_example1 :-
  448	nl,
  449	write(chang_lee_example1),
  450	clear,
  451	axioms([
  452		p(g(X,Y),X,Y),
  453		p(X,h(X,Y),Y),
  454		(p(U,Z,W) <= p(X,Y,U) and p(Y,Z,V) and p(X,V,W)),
  455		(p(X,V,W) <= p(X,Y,U) and p(Y,Z,V) and p(U,Z,W)),
  456		(query(X) <= p(k(X),X,k(X)))
  457	    ]),
  458	fail.				% clear stack used in compilation
  459chang_lee_example1 :-

  461	

  462	

  463	

 one

  464	prove_goal(query(_))

  464.
  465	
  466chang_lee_example2 :-
  467	nl,
  468	write(chang_lee_example2),nl,
  469	clear,
  470	axioms(
  471	[p(e,X,X),
  472	p(X,e,X),
  473	p(X,X,e),
  474	p(a,b,c),
  475	(p(U,Z,W) <= p(X,Y,U) and p(Y,Z,V) and p(X,V,W)),
  476	(p(X,V,W) <= p(X,Y,U) and p(Y,Z,V) and p(U,Z,W)),
  477	(query <= p(b,a,c))
  478	]),
  479	fail.
  480chang_lee_example2 :-
  481	prove_goal(query).
  482	
  483E