/* Automated Proof System */ % created: 27 Oct 2002. % modified: 28 Oct 2002. % modified: 31 Jul -- 3 Aug 2003. linear proof. % modified: 5-7 Aug 2003. mixed-initiative user interface. % although it is incomplete, yet bi-linear proof with mixed-initiative interface. % modified: 8-9 Aug 2003. tried bug fix. (on the problem of order sensitivity) % modified: 10 Aug 2003. bug fix above. The deduction theorem enabled. %reference: % [1] J.E.Bell and A.B.Slomson (1971). % Models and Ultraproducts:An Introduction. North-Holland. % pp.36-7. % [2] S. Arikawa and M. Haraguchi (1988). % Predicate Logic and Logic Programming. Ohm-sha.(Japanese) % deduce/2,3 : goals which can be proved in this system. % for example, % ?- deduce([]|-(a->a),B). % ?- deduce([a]|-(b->a),B). % ?- deduce([a,a->b]|-b,B). % ?- deduce([(a->b),(a->(b->c))]|-(a->c),B). % ?- deduce([a,(a->b),(b->c)]|-c,B). % ?- deduce([(a->b),(b->c)]|-(a->c),B). % ?- deduce([a,b,(a->(b->c))]|-(b->c),L). % proof/2 : the proofs by deduce/2 and deduce/3. % state_proof/1 : explain about the proof. % ?- state_proof(S). %------------------------ % basic axioms %------------------------ % axiom(sc1, [X,Y], (X -> (Y -> X))). axiom(sc2, [X,Y,Z], ((X -> (Y -> Z)) -> ((X -> Y) -> (X -> Z)))). axiom(sc3, [X,Y], ((\+ X -> \+ Y) -> (Y -> X))). /* axiom(sc4a, [X,Y], ((X, Y) -> X)). axiom(sc4b, [X,Y], ((X, Y) -> Y)). axiom(sc5, [X,Y,Z], ((X->Y)->((X->Z)->(X->(Y,Z))))). axiom(sc6a, [X,Y], (X -> (X ; Y))). axiom(sc6b, [X,Y], (Y -> (Y ; X))). axiom(sc7, [X,Y,Z], ((Y->X)->((Z->X)->((Y;Z)->X)))). axiom(ah(e), [X,Y], ((X->(Y->(X,Y))))). axiom(ah(e), [X,Y], ((X->Y)->((X-> \+ Y)-> \+ X))). */ %------------------------ % deduction rules %------------------------% :- dynamic user_goal/2. %:- dynamic theorem/4. user_goal(recent_index(0),dummy). current_user_goal(INDEX,G):- user_goal(INDEX,start(G)), INDEX=..[_|N], \+ ( user_goal(INDEX1,start(G)), INDEX1=..[_|N1], N1 < N ). theorem_0((B|-X),INDEX,P,Q):- user_goal(recent_index(INDEX), proved((B|-X),P,Q)), \+ self_reference_in_proof(X,Q). theorem((B|-X),INDEX,P,Q):- theorem_0((B|-X),INDEX,P,Q). theorem((B|-X),INDEX,P,Q):- user_goal(index(INDEX), proved((B|-X),P,Q)), \+ self_reference_in_proof(X,Q), \+ theorem_0((B|-X),_,_,_), \+ ( user_goal(index(INDEX1), proved((B|-X),_,Q1)), \+ self_reference_in_proof(X,Q1), INDEX1 < INDEX ). self_reference_in_proof(X,Q):- Q=(_,rules:Rules,_,_), member(theorem(X),Rules). % cf. proof/2 is the data of tentative achievement in a proof. init_user_goal:- abolish(user_goal/2), assert(user_goal(recent_index(0),dummy)). %-----deduce/2, deduce_1/2: reduced versions of deduce/3 deduce(Y,Q):- deduce(Y,_H,Q). deduce_1(Y,H):- deduce(Y,H,_Q). deduce(Y,H,Q):- (Y = (_ |- _)-> fail ; deduce(([] |- Y),H,Q) ). %-----deduce/3: logical reasoning with the user interface % modified: 4-8 Aug 2003. deduce(G,H,Q):- G=(_B |- _X), % set_user_goal update_with_index(user_goal,'++',_K,[start(G)]), % eliminate the previous data of session. preprocess_for_deduce, % do the job. deduce_0(G,H,Q), % terminate process update_proved_user_goal(G,H,Q). update_proved_user_goal(G,H,Q):- update_with_index(user_goal,'++',_K1,[proved(G,H,Q)]). %----- deduce_0/3: the rules for deduction: axioms and modus ponens deduce_0((B |- X),[P],Q):- member(N,[1,2,4,5]), deduce_pattern(N, (B|-X),S), P=(at_step(0),proved(X),using(S)), Q=(steps:[0],rules:[S],deduced:[X],inputs:[[]]), update_proof((B|-X),[P],Q). deduce_0((B |- Y),[P|H],Q):- length(H,L), (L >= 20->read(i);true), member([_COIN,INPUT1,INPUT2],[[0,X,(X->Y)],[1,(X->Y),X]]), member(N,[1,2,3,4,5]), deduce_pattern(N, (B |- INPUT1),S), \+ stopping_rule_0(H,L,[INPUT1,INPUT2]), deduce_0((B |- INPUT2), H, (_:L0,_:R1,_:R2,_:R3)), \+ member((_,proved(Y),_,_),H), stopping_rule(H,L,(B|-Y),[INPUT1,INPUT2],_), %\+ stopping_rule_1(H,L,[INPUT1,INPUT2]), P=(at_step(L),proved(Y),by_mp_from(INPUT2), using((INPUT1,S))), Q=(steps:[L|L0],rules:[S|R1],deduced:[Y|R2],inputs:[X|R3]), update_proof((B|-Y),[P|H],Q). /* % previous codes of the second deduce0/2: %-------------------------------------------------------- % note: the order of clauses is sensitive. deduce_0((B |- Y),[P|H],Q):- \+ member(Y,[(W->(W->_)),(W->(_->(W->_)))]), deduce_pattern(_N, (B|-(X->Y)),S), write(((B|-(X->Y)),mp(S))),user_confirm, deduce_0((B |- X), H, (_:L0,_:R1,_:R2,_:R3)), stopping(H,L,_), P=(at_step(L),proved(Y),by_mp_from(X->Y), using(S)), Q=(steps:[L|L0],rules:[S|R1],deduced:[Y|R2],inputs:[X|R3]), update_proof((B|-Y),[P|H],Q). deduce_0((B |- Y),[P|H],Q):- \+ member(Y,[(W->(W->_)),(W->(_->(W->_)))]), deduce_pattern(_N, (B|-X),S), write(((B|-X),mp(S))),user_confirm, deduce_0((B |- (X->Y)), H, (_:L0,_:R1,_:R2,_:R3)), stopping(H,L,_), P=(at_step(L),proved(Y),by_mp_from(X->Y), using(S)), Q=(steps:[L|L0],rules:[S|R1],deduced:[Y|R2],inputs:[X|R3]), update_proof((B|-Y),[P|H],Q). %-------------------------------------------------------- */ %----- filtration possible_deduce_patterns( [ user, deduction_theorem, theorem, assumption, proved, axiom ] ). deduce_pattern(N,(B|-X),Case):- var(B), !, B=[], deduce_pattern(N,(B|-X),Case). deduce_pattern(N,(B|-X),Case):- possible_deduce_patterns(Patterns), member(F,Patterns), Case =.. [F,_], deduce_pattern(N,(B|-X),Case,Exec), user_confirm_by_deduce_mode((B|-X),Case), %nl,write(Case), % delayed execution Exec. %----- patterns deduce_pattern(1,(B|-X),assumption(X),true):- % \+ var(B), member(X,B). deduce_pattern(2,(_B|-X),axiom(A),true):- axiom(A, _, X). deduce_pattern(3,(_B|-X),proved(X),true):- clause(proof( _, deduced:D),true), \+ var(D), member(X,D). deduce_pattern(4,(B|-X),theorem(X),true):- theorem((A|-X),_,_,_), subset(A,B). deduce_pattern(4,(B|-(X->Y)),deduction_theorem(X),true):- theorem((A|-Y),_,_,_), member(X,A), subset(B,A). deduce_pattern(4,(B|-(X->Y)),deduction_theorem(X),true):- theorem((A|-Y),_,_,_), member(X,A), subset(B,A). deduce_pattern(5,(_B|-X),user(X),Exec):- Exec = user_confirm((X,'as the oracle?')). %----- deduce_mode/3 as the filter for deduce/3, % which is applied at user_confirm_by_deduce_mode/1. :- dynamic deduce_mode/3. % note: a deduce_mode is updated by using % update_deduce_mode/3 in the later part of the program. %mode deduce_mode(auto_confirm,mode,off). %permission deduce_mode(auto_confirm,allow,axiom(sc1)). deduce_mode(auto_confirm,allow,axiom(sc2)). deduce_mode(auto_confirm,allow,axiom(sc3)). deduce_mode(auto_confirm,allow,proved(_)). deduce_mode(auto_confirm,allow,assumption(_)). %inhibit deduce_mode(auto_confirm,inhibit,user(_)). deduce_mode(auto_confirm,set(A),B):- member(A,[allow,inhibit]), findall(S,deduce_mode(auto_confirm,A,S),B). %----- stopping criteria. stop(inference_bound,10). stop(confirmation_bound,5000). stopping_rule(H,_L,Y,INPUTS,Return):- ( stopping_rule_0(H,Y,INPUTS); stopping_rule_1(H,Y,INPUTS) ), !, Return= stop. stopping_rule(_H,_L,_Y,_,continue). stopping_rule_0(H,_Y,_INPUTS,stop):- length(H,K), stop(inference_bound,TB), K >= TB, write('<>'), read(c). stopping_rule_0(_H,_Y,_INPUTS):- user_confirm_data(recent_index(IX),_,_), stop(confirmation_bound,IXB), IX >= IXB, write('<>'), read(c). stopping_rule_1(_H,_Y,_INPUTS):- current_user_goal(_,(B|-X)), proof((B|-X),_), %member((_,proved(X),_,_),H), write('<< serendipity stop >> case(1) --- the goal '), write(X), write(' has been proved accidently in this proof.'), read(c), proved(G,H,Q), update_proved_user_goal(G,H,Q). stopping_rule_1(_H,_Y,INPUTS):- member(X,INPUTS), current_user_goal(_,(B|-X)), proof((B|-X),_), write('<< serendipity stop >> case(2) --- the input '), write(X), write(' for mp is the goal previously proved.'), read(c). stopping_rule_1(_H,(B|-Y),_INPUTS):- proof((B|-Y),_), write('<< serendipity stop >> case(3) --- the subgoal '), write(Y), write(' was already proved in the proof.'), read(c). %----- old stopping rule. stopping(H,L,Y):- \+var(H), \+ (member(X,H),var(X)), length(H,L), stop(T), (L >= T -> (Y=yes,trim_stacks,write('the time (Ctl+c)'));Y=no). stopping(H,_L,yes):- var(H),write(stop), read(y). % reference to the preivious goal -------- proved(Goal, H, Data):- clause(proof(Goal, story:H),_), Data=(steps:L,rules:R,deduced:D,inputs:I), proof(Goal, steps:L), proof(Goal, rules:R), proof(Goal, deduced:D), proof(Goal, inputs:I). % updating proof------------------------- :- dynamic proof/2. % note: proof/2 and user_confirm_data. %----------------------------------------- % Although proof/2 and user_confirm_data are both tentative background data, they have different perspectives respectively. % proof/2 is localized within a deduce_0/3, i.e., they are updated by each step of the proof, whereas % user_confirm/2 is localized within a deduce/3, i.e., they are updated by each goal specified by the user. % cf., user_goal/2 accumulates the proving efforts by a success of deduce/3. update_proof(Goal,[P],Data):- Data=(steps:[S],rules:[A],deduced:[D],inputs:[Imp]), assert(proof(Goal,story:[P])), assert(proof(Goal,steps:[S])), assert(proof(Goal,rules:[A])), assert(proof(Goal,deduced:[D])), assert(proof(Goal,inputs:[Imp])). update_proof(Goal,[P|H],Data):- Data=(Steps,Rules,Deduced,Inputs), Steps = steps:[_S|X1], Rules = rules:[_A|X2], Deduced = deduced:[_D|X3], Inputs = inputs:[_I|X4], Data0 = (steps:X1,rules:X2,deduced:X3,inputs:X4), Goal=(B|-_), proved((B|-_G0), H, Data0), abolish(proof/2), assert(proof(Goal,story:[P|H])), assert(proof(Goal,Steps)), assert(proof(Goal,Rules)), assert(proof(Goal,Deduced)), assert(proof(Goal,Inputs)). %provable((A -> A)). lemma(16,P):- deduce(([]|-(a->a)),P), listing(proof). % proof: % In these axioms, you may see a sc1 as the lhs subformula in sc2, % and an objective-like formula, but it is A->A instead of A per se, % appears in the rhs if X is true and Y=Z. % From sc2 /[A,(A->A),A], sc1/[A,(A->A)], we get (A->[A->A])->(A->A). % Again from sc1 /[A,A] the formula has attained. %----------------------------------------- % display of proofs %----------------------------------------- % modified: 8 Aug 2003. %-----explanation for proof/2, the records of deduce/2,3. state_proof(G):- \+ var(G), G=theorem, theorem(Goal,_,Proof,_), state_proof(Goal,Proof). state_proof(Goal):- \+ var(Goal), user_goal(_,proved(Goal,_,Proof,_)), !, state_proof(Goal,Proof). state_proof(INDEX):- \+ var(INDEX), user_goal(INDEX,proved(Goal,_,Proof,_)), !, state_proof(Goal,Proof). state_proof(Goal):- state_current_proof(Goal). state_current_proof(Goal):- proof(Goal,story:Proof), state_proof(Goal,Proof). state_proof(Goal,Proof):- nl,write(target(Goal)), forall(member(X,Proof), ( X=(at_step(L),proved(G),M), nl,tab(1), write(at_step(L)), tab(3), write(proved(G)), nl,tab(3), write(M) ) ). forall_write(X,G):- forall(G,(nl,write(X))). %------------------------------------------- % user control and stopping rule. %------------------------------------------- %----- a mixed initiative strategies for the user interface. % added: 5 Aug 2003. % modified: 6-10 Aug 2003. :- dynamic user_confirm_data/3. user_confirm_data(recent_index(0),init,dummy). current_user_confirm_data(INDEX,A,B):- user_confirm_data(recent_index(INDEX),A,B). user_confirm_by_deduce_mode(G,S):- deduce_mode(auto_confirm, mode,off), !, user_confirm((G,S)). user_confirm_by_deduce_mode(_,S):- deduce_mode(auto_confirm, mode,on), deduce_mode(auto_confirm, inhibit,S), !, fail. user_confirm_by_deduce_mode(G,S):- deduce_mode(auto_confirm, mode,on), deduce_mode(auto_confirm, allow,S), !, update_user_confirm_data((G,S)). user_confirm_by_deduce_mode(G,S):- user_confirm((G,S)). user_confirm:- write(' (y.)>'), read(Y), (Y=y->true;fail). user_confirm(Mes):- nl,write((Mes,'go ahead ?') ), user_confirm, update_user_confirm_data(Mes). update_user_confirm_data(Mes):- user_confirm_data(recent_index(K),_,_), update_with_index(user_confirm_data,'++',K,[auto_confirm,Mes]). % common utility: update_with_index(GF,'++',K,D) %------------------------------------------- update_with_index(GF,'++',K,D):- length(D,L), length(D0,L), PRE=..[GF|[recent_index(K)|D0]], OLD=..[GF|[index(K)|D0]], ( retract(PRE) -> assert(OLD) ; ( K=0, D0=[dummy|_], Dummy =..[GF|[index(K)|D0]], assert(Dummy) ) ), K1 is K + 1, NEW=..[GF|[recent_index(K1)|D]], assert(NEW). %------------------------------------------- % setting the mode for deduction. %------------------------------------------- % added: 6 Aug 2003. % modified: 7-8 Aug 2003. %----- the preprocess for deduce0/3 that is used in deduced/3. preprocess_for_deduce:- setting_user_controls, init_privious_proof_data, init_user_confirm_data. setting_user_controls:- ask_user_whether_to_keep_records_or_not, ask_user_whether_to_trace_using_proved_or_not. init_privious_proof_data:- abolish(proof/2). init_user_confirm_data:- abolish(user_confirm_data/3), assert(user_confirm_data(recent_index(0),init,dummy)). % to set deduce mode %-------------------- ask_user_whether_to_keep_records_or_not:- clause(user_goal(index(1),_),_), !, ask_user_whether_to_keep_records_or_not_1. ask_user_whether_to_keep_records_or_not. ask_user_whether_to_keep_records_or_not_1:- user_confirm('Will you keep the previous results ?'), !, % alow deduce_patterns which refer succeeded goals (i.e., theorems). update_deduce_mode(auto_confirm,add,allow:theorem(_)). ask_user_whether_to_keep_records_or_not_1:- user_confirm('All proved theorems will be kept but not to be used.'), !, % inhibit deduce_patterns using theorems. update_deduce_mode(auto_confirm,add,inhibit:theorem(_)). ask_user_whether_to_keep_records_or_not_1:- ask_user_whether_to_keep_records_or_not. % to set confirmation mode %-------------------- ask_user_whether_to_trace_using_proved_or_not:- \+ deduce_mode(auto_confirm,mode,off), user_confirm('use the auto-confirmation mode ?'), !, update_deduce_mode(auto_confirm,mode,on), ask_user_whether_to_trace_using_proved_or_not_1. ask_user_whether_to_trace_using_proved_or_not:- user_confirm( '% nothing will be passed without the confirmation by user? ' ), user_confirm( '% And nothing will be pruned by the preconditions? ' ), deduce_mode(auto_confirm,set(allow),A), deduce_mode(auto_confirm,set(inhibit),B), warn_user_about_deduce_mode_if([A,B],_), update_deduce_mode(auto_confirm,mode,off). ask_user_whether_to_trace_using_proved_or_not:- update_deduce_mode(auto_confirm,mode,on), ask_user_whether_to_trace_using_proved_or_not. ask_user_whether_to_trace_using_proved_or_not_1:- PrintA=(nl,tab(3),write((allow:A))), deduce_mode(auto_confirm,set(allow),A),PrintA, PrintB=(nl,tab(3),write((inhibit:B))), deduce_mode(auto_confirm,set(inhibit),B),PrintB, forall(warn_user_about_deduce_mode_if([A,B],T),T=true), user_confirm('use these conditions ?'). ask_user_whether_to_trace_using_proved_or_not_1:- nl, nl, M1= 'input new conditions as ', M2= 'add(allow,axiom(sc1)), ', M3= 'remove(inhibit,assumption(a)), ', M4= 'or end :', forall(member(X,[M1,M2,M3,M4]), write(X)), nl, read(U), ask_user_whether_to_trace_using_proved_or_not_2(U). ask_user_whether_to_trace_using_proved_or_not_2(end). ask_user_whether_to_trace_using_proved_or_not_2(G):- G=..GL, member(GL,[[F,X,Y],[F,(X:Y)]]), member(F,[add,remove]), member(X,[allow,inhibit]), member(Y,[axiom(A),assumption(A),proved(A)]), update_deduce_mode(auto_confirm,F,X:Y), ask_user_whether_to_trace_using_proved_or_not_1. warn_user_about_deduce_mode_if([A,B],fail):- \+ (intersection(A,B,[])), nl, Warning1 = 'specified conditions are conflicting. ', Warning2 = 'please re-enter.', forall(member(X,['!! ',Warning1,Warning2]),write(X)). warn_user_about_deduce_mode_if([[],[]],true):- % nothing will be passed without the confirmation by user, % and nothing will be pruned by the preconditions. nl, Warning1 = 'you shall type a (y.) for each inference ', Warning2 = 'because the conditions are vacuous.', forall(member(X,['!! ',Warning1,Warning2]),write(X)). warn_user_about_deduce_mode_if(_,true). %update deduce_mode/3 %---------------------------------------------- update_deduce_mode(auto_confirm,remove,F:G):- \+ var(F), member(F,[allow,inhibit]), retractall( deduce_mode(auto_confirm,F,G) ). update_deduce_mode(auto_confirm,add,F:G):- member([allow,inhibit],[[F,H],[H,F]]), update_deduce_mode(auto_confirm,remove,F:G), assert( deduce_mode(auto_confirm,F,G) ), update_deduce_mode(auto_confirm,remove,H:G). update_deduce_mode(auto_confirm,mode,off):- retractall(deduce_mode(auto_confirm,mode,_)), assert(deduce_mode(auto_confirm,mode,off)). update_deduce_mode(auto_confirm,mode,on):- retractall(deduce_mode(auto_confirm,mode,_)), assert(deduce_mode(auto_confirm,mode,on)). update_deduce_mode(auto_confirm,_,_):- nl,write(' what ? lets try again.'), fail. %----------------------------------------- % sample executions %----------------------------------------- /* ?- [pcaxiom01]. % pcaxiom01 compiled 0.01 sec, -2,628 bytes Yes ?- deduce(([a]|-(b->a)),B). ([a]|- (a->b->a)), mp(assumption) try this ? (y.)>y. ([a]|- (a->b->a)), by_axiom(sc1) try this ? (y.)>y. B = steps:[1, 0], rules:[assumption, sc1], deduced:[ (b->a), (a->b->a)], inputs:[a, []] Yes ?- state_proof(G). target(([a]|- (b->a))) at_step(1) proved((b->a)) by_mp_from((a->b->a)), using(assumption) at_step(0) proved((a->b->a)) using(axiom(sc1)) G = [a]|- (b->a) Yes ?- deduce([]|-(a->a),L). level(0), ([]|- (_G272->_G275->_G272)), mp(axiom(sc1)) level(1), ([]|- (_G272->_G275->_G272)), mp(axiom(sc1)) level(0), ([]|- (_G464->_G467->_G464)), mp(axiom(sc1)) level(0), ([]|- ((_G464->_G467->_G470)-> (_G464->_G467)->_G464->_G470)), mp(axiom(sc2)) level(0), ([]|- ((\+_G464-> \+_G467)->_G467->_G464)), mp(axiom(sc3)) level(0), ([]|- ((a->a)-> (_G272->_G275->_G272)->a->a)), mp(axiom(sc1)) level(0), ([]|- ((a-> (_G275->a)->a)-> (a->_G275->a)->a->a)), mp(axiom(sc2)) level(0), ([]|- ((\+ (a->a)-> \+ (_G272->_G275->_G272))-> (_G272->_G275->_G272)->a->a)), mp(axiom(sc3)) level(2), ([]|- (_G272->_G275->_G272)), mp(axiom(sc1)) level(1), ([]|- (_G517->_G520->_G517)), mp(axiom(sc1)) ([]|- ((a-> (_G275->a)->a)-> (a->_G275->a)->a->a)), axiom(sc2) L = steps:[2, 1, 0], rules:[axiom(sc1), axiom(sc1), axiom(sc2)], deduced:[ (a->a), ((a->_G275->a)->a->a), ((a->... ->...)-> (... ->...)->... ->...)], inputs:[ (a->_G275->a), (a-> (_G275->a)->a), []] Yes ?- state_proof(I). target(([]|- (a->a))) at_step(2) proved((a->a)) by_mp_from(((a->_G243->a)->a->a)), using(((a->_G243->a), axiom(sc1))) at_step(1) proved(((a->_G243->a)->a->a)) by_mp_from(((a-> (_G243->a)->a)-> (a->_G243->a)->a->a)), using(((a-> (_G243->a)->a), axiom(sc1))) at_step(0) proved(((a-> (_G243->a)->a)-> (a->_G243->a)->a->a)) using(axiom(sc2)) I = []|- (a->a) Yes ?- listing(proof). :- dynamic proof/2. proof(([a, (a->b)]|-b), story:[ (at_step(1), proved(b), by_mp_from((a->b)), using(assumption)), (at_step(0), proved((a->b)), using(assumption))]). proof(([a, (a->b)]|-b), steps:[1, 0]). proof(([a, (a->b)]|-b), rules:[assumption, assumption]). proof(([a, (a->b)]|-b), deduced:[b, (a->b)]). proof(([a, (a->b)]|-b), inputs:[a, []]). Yes ?- deduce([a->b,b->c]|-(a->c),L). %<-----omit-----> level(0), ([ (a->b), (b->c)]|- ((\+_G1030-> \+_G1033)->_G1033->_G1030)), mp(axiom(sc3)) level(0), ([ (a->b), (b->c)]|- ((a->b->c)-> (a->b)->a->b->c)), mp(axiom(sc1)) level(0), ([ (a->b), (b->c)]|- ((a->b->b->c)-> (a->b)->a->b->c)), mp(axiom(sc2)) level(0), ([ (a->b), (b->c)]|- ((\+ (a->b->c)-> \+ (a->b))-> (a->b)->a->b->c)), mp(axiom(sc3)) level(1), ([ (a->b), (b->c)]|- (b->c)), mp(assumption) ([ (a->b), (b->c)]|- ((b->c)->a->b->c)), axiom(sc1) L = steps:[3, 2, 1, 0], rules:[assumption, axiom(sc2), assumption, axiom(sc1)], deduced:[ (a->c), ((a->b)->a->c), (a->b->c), ((... ->...)->... ->...)], inputs:[ (a->b), (a->b->c), (b->c), []] Yes ?- state_proof(I). target(([ (a->b), (b->c)]|- (a->c))) at_step(3) proved((a->c)) by_mp_from(((a->b)->a->c)), using(((a->b), assumption)) at_step(2) proved(((a->b)->a->c)) by_mp_from((a->b->c)), using((((a->b->c)-> (a->b)->a->c), axiom(sc2))) at_step(1) proved((a->b->c)) by_mp_from(((b->c)->a->b->c)), using(((b->c), assumption)) at_step(0) proved(((b->c)->a->b->c)) using(axiom(sc1)) I = [ (a->b), (b->c)]|- (a->c) Yes L = steps:[2, 1, 0], rules:[assumption, proved(((a->b)->a->c)), assumption], deduced:[c, (a->c), (a->b)], inputs:[a, (a->b), []] Yes ?- deduce([a,a->b,b->c]|- (c),L). L = steps:[2, 1, 0], rules:[assumption, proved(((a->b)->a->c)), assumption], deduced:[c, (a->c), (a->b)], inputs:[a, (a->b), []] Yes ?- state_proof(A). target(([a, (a->b), (b->c)]|-c)) at_step(2) proved(c) by_mp_from((a->c)), using((a, assumption)) at_step(1) proved((a->c)) by_mp_from((a->b)), using((((a->b)->a->c), proved(((a->b)->a->c)))) at_step(0) proved((a->b)) using(assumption) A = [a, (a->b), (b->c)]|-c Yes % user-specified sequence. %----------- user confirmation mode: ?- deduce([(a->b),(a->(b->c))]|-(a->c),B). ([ (a->b), (a->b->c)]|- ((a->b)->a->c)), mp(assumption) (y.)>y. ([ (a->b), (a->b->c)]|- ((a->b)-> (a->b)->a->c)), mp(assumption) (y.)>y. ([ (a->b), (a->b->c)]|- ((a->b->c)-> (a->b)->a->c)), mp(assumption) (y.)>y. ([ (a->b), (a->b->c)]|- ((a->b->c)-> (a->b)->a->c)), by_axiom(sc2) (y.)>y. B = steps:[2, 1, 0], rules:[assumption, assumption, sc2], deduced:[ (a->c), ((a->b)->a->c), ((a->... ->...)-> (... ->...)->... ->...)], inputs:[ (a->b), (a->b->c), []] Yes ?- state_proof(G). target(([ (a->b), (a->b->c)]|- (a->c))) at_step(2) proved((a->c)) by_mp_from(((a->b)->a->c)), using(assumption) at_step(1) proved(((a->b)->a->c)) by_mp_from(((a->b->c)-> (a->b)->a->c)), using(assumption) at_step(0) proved(((a->b->c)-> (a->b)->a->c)) using(axiom(sc2)) G = [ (a->b), (a->b->c)]|- (a->c) Yes ([a, (a->b), (a->b->c)]|- (a->c)), mp(assumption) try this ? (y.)>y. ([a, (a->b), (a->b->c)]|- (a->a->c)), mp(assumption) try this ? (y.)>y. ([a, (a->b), (a->b->c)]|- ((a->b)->a->c)), mp(assumption) try this ? (y.)>y. ([a, (a->b), (a->b->c)]|- (a-> (a->b)->a->c)), mp(assumption) try this ? (y.)>y. ([a, (a->b), (a->b->c)]|- ((a->b)-> (a->b)->a->c)), mp(assumption) try this ? (y. ([a, (a->b), (a->b->c)]|- ((a->b->c)-> (a->b)->a->c)), mp(assumption) try this y. ([a, (a->b), (a->b->c)]|- ((a->b->c)-> (a->b)->a->c)), by_axiom(sc2) try this ?y. B = steps:[3, 2, 1, 0], rules:[assumption, assumption, assumption, sc2], deduced:[c, (a->c), ((a->b)->a->c), ((... ->...)->... ->...)], inputs:[a, (a->b), (a->b->c), []] Yes ?- state_proof(A). target(([a, (a->b), (a->b->c)]|-c)) at_step(3) proved(c) by_mp_from((a->c)), using(assumption) at_step(2) proved((a->c)) by_mp_from(((a->b)->a->c)), using(assumption) at_step(1) proved(((a->b)->a->c)) by_mp_from(((a->b->c)-> (a->b)->a->c)), using(assumption) at_step(0) proved(((a->b->c)-> (a->b)->a->c)) using(axiom(sc2)) A = [a, (a->b), (a->b->c)]|-c Yes % Mixed-Initiative Strategy (user-confirmation) mode % case 1 (default): total freedom. nothing to be inspected. %---------------------------------------------------------- ?- deduce(a->a,L). use the auto-confirmation mode ?, go ahead ? (y.)>y. allow:[axiom(sc1), axiom(sc2), axiom(sc3), proved(_G327), assumption(_G319)] inhibit:[] use these conditions ?, go ahead ? (y.)>y. L = steps:[2, 1, 0], rules:[axiom(sc1), axiom(sc1), axiom(sc2)], deduced:[ (a->a), ((a->_G511->a)->a->a), ((a->... ->...)-> (... ->...)->... ->...)], inputs:[ (a->_G511->a), (a-> (_G511->a)->a), []] Yes % case 2 (deny promptly): total censorship. %---------------------------------------------------------- ?- deduce([a]|-a,L). use the auto-confirmation mode ?, go ahead ? (y.)>n. % nothing will be passed without the confirmation by user, % and nothing will be pruned by the preconditions. (([a]|-a), assumption(a)), go ahead ? (y.)>y. L = steps:[0], rules:[assumption(a)], deduced:[a], inputs:[[]] Yes input new conditions as add(allow,axiom(sc1)), remove(inhibit,assumption(a)), or end : | remove(allow:axiom(sc3)). allow:[axiom(sc1), axiom(sc2), proved(_G489), assumption(_G481)] inhibit:[] use these conditions ?, go ahead ? (y.)>n. % case 3 (mixed initiative mode): some cases. %---------------------------------------------------------- ?- deduce([a]|-a,L). Will you keep the previous results ?, go ahead ? (y.)>n. use the auto-confirmation mode ?, go ahead ? (y.)>y. allow:[axiom(sc1), axiom(sc2), axiom(sc3), proved(_G395), assumption(_G387)] inhibit:[] use these conditions ?, go ahead ? (y.)>n. input new conditions as add(allow,axiom(sc1)), remove(inhibit,assumption(a)), or end : | remove(allow:proved(_)). allow:[axiom(sc1), axiom(sc2), assumption(_G575)] inhibit:[] use these conditions ?, go ahead ? (y.)>y. L = steps:[0], rules:[assumption(a)], deduced:[a], inputs:[[]] Yes ?- state_proof(A). target(([a]|-a)) at_step(0) proved(a) using(assumption(a)) A = [a]|-a Yes ?- deduce([a,a->b,b->c]|-(c),L). use the auto-confirmation mode ?, go ahead ? (y.)>y. allow:[axiom(sc1), axiom(sc2), assumption(_G353)] inhibit:[] use these conditions ?, go ahead ? (y.)>n. input new conditions as add(allow,axiom(sc1)), remove(inhibit,assumption(a)), or end : | add(inhibit:axiom(sc3)). allow:[axiom(sc1), axiom(sc2), assumption(_G460)] inhibit:[axiom(sc3)] use these conditions ?, go ahead ? (y.)>y. L = steps:[4, 3, 2, 1, 0], rules:[assumption(a), assumption((a->b)), axiom(sc2), assumption((b->c)), axiom(sc1)], deduced:[c, (a->c), ((a->b)->a->c), (a->... ->...), (... ->...)], inputs:[a, (a->b), (a->b->c), (b->c), []] Yes ?- state_proof(I). target(([a, (a->b), (b->c)]|-c)) at_step(4) proved(c) by_mp_from((a->c)), using((a, assumption(a))) at_step(3) proved((a->c)) by_mp_from(((a->b)->a->c)), using(((a->b), assumption((a->b)))) at_step(2) proved(((a->b)->a->c)) by_mp_from((a->b->c)), using((((a->b->c)-> (a->b)->a->c), axiom(sc2))) at_step(1) proved((a->b->c)) by_mp_from(((b->c)->a->b->c)), using(((b->c), assumption((b->c)))) at_step(0) proved(((b->c)->a->b->c)) using(axiom(sc1)) I = [a, (a->b), (b->c)]|-c Yes ?- deduce([a->b,b->c]|-(a->c),L). Will you keep the previous results ?, go ahead ? (y.)>n. use the auto-confirmation mode ?, go ahead ? (y.)>y. allow:[axiom(sc1), axiom(sc2), assumption(_G592)] inhibit:[axiom(sc3)] use these conditions ?, go ahead ? (y.)>y. L = steps:[3, 2, 1, 0], rules:[assumption((a->b)), axiom(sc2), assumption((b->c)), axiom(sc1)], deduced:[ (a->c), ((a->b)->a->c), (a->b->c), ((... ->...)->... ->...)], inputs:[ (a->b), (a->b->c), (b->c), []] Yes ?- state_proof(I). target(([ (a->b), (b->c)]|- (a->c))) at_step(3) proved((a->c)) by_mp_from(((a->b)->a->c)), using(((a->b), assumption((a->b)))) at_step(2) proved(((a->b)->a->c)) by_mp_from((a->b->c)), using((((a->b->c)-> (a->b)->a->c), axiom(sc2))) at_step(1) proved((a->b->c)) by_mp_from(((b->c)->a->b->c)), using(((b->c), assumption((b->c)))) at_step(0) proved(((b->c)->a->b->c)) using(axiom(sc1)) I = [ (a->b), (b->c)]|- (a->c) Yes ?- deduce([a,b,(a->(b->c))]|-(b->c),L). Will you keep the previous results ?, go ahead ? (y.)>n. All proved theorems will be kept but not to be used., go ahead ? (y.)>y. % nothing will be passed without the confirmation by user, % and nothing will be pruned by the preconditions. ok, go ahead ? (y.)>n. allow:[axiom(sc1), axiom(sc2), axiom(sc3), proved(_G598), assumption(_G590)] inhibit:[user(_G678), theorem(_G670)] use these conditions ?, go ahead ? (y.)>y. at_step(0), proved((a->b->c)), using(assumption((a->b->c))) L = steps:[1, 0], rules:[assumption(a), assumption((a->b->c))], deduced:[ (b->c), (a->b->c)], inputs:[a, []] Yes ?- state_proof(I). target(([a, b, (a->b->c)]|- (b->c))) at_step(1) proved((b->c)) by_mp_from((a->b->c)), using((a, assumption(a))) at_step(0) proved((a->b->c)) using(assumption((a->b->c))) I = [a, b, (a->b->c)]|- (b->c) Yes %---- using theorems ?- deduce([a,a->b]|-b,L). Will you keep the previous results ?, go ahead ? (y.)>n. All proved theorems will be kept but not to be used., go ahead ? (y.)>y. use the auto-confirmation mode ?, go ahead ? (y.)>y. allow:[axiom(sc1), axiom(sc2), axiom(sc3), proved(_G777), assumption(_G769)] inhibit:[user(_G857), theorem(_G849)] use these conditions ?, go ahead ? (y.)>y. L = steps:[1, 0], rules:[assumption(a), assumption((a->b))], deduced:[b, (a->b)], inputs:[a, []] Yes ?- user_confirm_data(recent_index(I),A,C). I = 19 A = auto_confirm C = ([a, (a->b), (b->c)]|- (a->b)), assumption((a->b)) Yes ?- deduce([a,a->b,b->c]|-c,L). Will you keep the previous results ?, go ahead ? (y.)>y. % nothing will be passed without the confirmation by user, % and nothing will be pruned by the preconditions. ok, go ahead ? (y.)>n. use the auto-confirmation mode ?, go ahead ? (y.)>y. allow:[axiom(sc1), axiom(sc2), axiom(sc3), proved(_G646), assumption(_G638), theorem(_G630)] inhibit:[user(_G718)] use these conditions ?, go ahead ? (y.)>y. L = steps:[1, 0], rules:[theorem(b), assumption((b->c))], deduced:[c, (b->c)], inputs:[b, []] Yes ?- user_confirm_data(recent_index(I),A,C). I = 70 A = auto_confirm C = ([a, (a->b), (b->c)]|- (b->c)), assumption((b->c)) Yes ?- theorem(A,B,C,D). A = [a, (a->b), (b->c)]|-c B = 5 C = [ (at_step(1), proved(c), by_mp_from((b->c)), using((b, theorem(b)))), (at_step(0), proved((b->c)), using(assumption((b->c))))] D = steps:[1, 0], rules:[theorem(b), assumption((b->c))], deduced:[c, (b->c)], inputs:[b, []] ; A = [a, (a->b)]|-b B = 2 C = [ (at_step(1), proved(b), by_mp_from((a->b)), using((a, assumption(a)))), (at_step(0), proved((a->b)), using(assumption((a->b))))] D = steps:[1, 0], rules:[assumption(a), assumption((a->b))], deduced:[b, (a->b)], inputs:[a, []] ; No ?- deduce([a,a->b,b->c]|-c,L). Will you keep the previous results ?, go ahead ? (y.)>n. All proved theorems will be kept but not to be used., go ahead ? (y.)>y. use the auto-confirmation mode ?, go ahead ? (y.)>y. allow:[axiom(sc1), axiom(sc2), axiom(sc3), proved(_G738), assumption(_G730)] inhibit:[user(_G818), theorem(_G810)] use these conditions ?, go ahead ? (y.)>y. <>c. <>c. L = steps:[2, 1, 0], rules:[assumption((b->c)), assumption(a), assumption((a->b))], deduced:[c, b, (a->b)], inputs:[b, a, []] Yes ?- user_confirm_data(recent_index(I),A,C). I = 514 A = auto_confirm C = ([a, (a->b), (b->c)]|- (a->b)), assumption((a->b)) Yes % the serendipity stop: a bug in privious version(8 Aug) %---------------------------------------- ?- deduce([a->b,a]|-b,L). Will you keep the previous results ?, go ahead ? (y.)>n. use the auto-confirmation mode ?, go ahead ? (y.)>y. allow:[axiom(sc1), axiom(sc2), axiom(sc3), proved(_G500), assumption(_G492)] inhibit:[] use these conditions ?, go ahead ? (y.)>y. <> % <--- Action (h for help) ? abort % <--- % Execution Aborted ?- state_proof(A). target(([ (a->b), a]|- ((a->b)->b))) at_step(2) proved(((a->b)->b)) by_mp_from(b), using(((b-> (a->b)->b), axiom(sc1))) at_step(1) proved(b) by_mp_from((a->b)), using((a, assumption(a))) at_step(0) proved((a->b)) using(assumption((a->b))) A = [ (a->b), a]|- ((a->b)->b) Yes ?- deduce([a->b,a,b->c]|-c,L). Will you keep the previous results ?, go ahead ? (y.)>y. use the auto-confirmation mode ?, go ahead ? (y.)>y. allow:[axiom(sc1), axiom(sc2), axiom(sc3), proved(_G525), assumption(_G517)] inhibit:[] use these conditions ?, go ahead ? (y.)>y. <> Action (h for help) ? abort % Execution Aborted ?- state_proof(A). target(([ (a->b), a, (b->c)]|- ((a->b)->c))) at_step(2) proved(((a->b)->c)) by_mp_from(c), using(((c-> (a->b)->c), axiom(sc1))) at_step(1) proved(c) by_mp_from((b->c)), using((b, proved(b))) at_step(0) proved((b->c)) using(assumption((b->c))) A = [ (a->b), a, (b->c)]|- ((a->b)->c) Yes ?- deduce([c]|-c,L). Will you keep the previous results ?, go ahead ? (y.)>y. use the auto-confirmation mode ?, go ahead ? (y.)>y. allow:[axiom(sc1), axiom(sc2), axiom(sc3), proved(_G500), assumption(_G492)] inhibit:[user(_G572)] use these conditions ?, go ahead ? (y.)>y. L = steps:[0], rules:[assumption(c)], deduced:[c], inputs:[[]] ; (([c]|-c), theorem(c)), go ahead ? (y.)>y. L = steps:[0], rules:[theorem(c)], deduced:[c], inputs:[[]] Yes ?- */ %-----------------------------------------