/* 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
?- 
*/
%-----------------------------------------

return to front page.