/* changes:
 * 7/3/03: indent_node/3 reuired non-empty list for 1st argument
 */

/*
 *  Do not change the code for the inference rules;
 *  any search method that produces derivations in the
 *  specified syntax is fine.
 */

/* Prolog version of inference rules for S4 propositional logic.

   Run under DICE sicstus

   uses multiple conclusion sequents, pairs of lists of wffs, read as
   "if all the wffs in first list are true, then some wff in the second
    list is true".

    Example query: which rules apply?

?- rule( R, [ [a=>e, c \/ c2, #e, ~f] ==> [b => a, #h], incomplete ], B, C ).
B = [[a=>e,c\/c2,#e,~f]==>[b=>a,#h],orE(2)],
C = [[[a=>e,c,#e,~f]==>[b=>a,#h],incomplete],[[a=>e,c2,#e,~f]==>[b=>a,#h],incomplete]],
R = orE(2) ? ;

B = [[a=>e,c\/c2,#e,~f]==>[b=>a,#h],impI(1)],
C = [[[b,a=>e,c\/c2,#e,~f]==>[a,#h],incomplete]],
R = impI(1) ? ;

B = [[a=>e,c\/c2,#e,~f]==>[b=>a,#h],impE(1)],
C = [[[c\/c2,#e,~f]==>[a,b=>a,#h],incomplete],[[e,c\/c2,#e,~f]==>[b=>a,#h],incomplete]],
R = impE(1) ? ;

B = [[a=>e,c\/c2,#e,~f]==>[b=>a,#h],notE(4)],
C = [[[a=>e,c\/c2,#e]==>[f,b=>a,#h],incomplete]],
R = notE(4) ? ;

B = [[a=>e,c\/c2,#e,~f]==>[b=>a,#h],boxI(2)],
C = [[[e]==>[h],incomplete]],
R = boxI(2) ? ;

B = [[a=>e,c\/c2,#e,~f]==>[b=>a,#h],boxE(3)],
C = [[[a=>e,c\/c2,e,~f]==>[b=>a,#h],incomplete]],
R = boxE(3) ? ;
no

    Solutions given in order in which the rules appear in the code.

    These should be used to build a derivation for a given sequent;
    derivations are trees, represented by terms of the shape:

    der( [ Seq, axiom], [] )
                where seq is an axioms, or
    der( [ Seq, incomplete], [] )
                marking an open leaf, or
    der( [ Seq, Rule ], [ der( Seq1, Y ) ] )
                where der( Seq1, Y ) is a derivation, and
		      Rule relates Seq1 to Seq; or
    der( [ Seq, Rule ], [ der( Seq1, Y1), der( Seq2, Y2 ) ] )
                 where Rule relates Seq1 and Se2 to Seq, and
		 der(Seq1, Y1), der(Seq2, Y2) are derivations.

*/

/*

   List utilities 
*/

member(X,[X|_]).
member(X,[_|T]) :- member(X,T).
append([],X,X).
append([H|T],X,[H|Y]) :- append(T,X,Y).

reverse(In,Out) :- rev2(In,[],Out).
rev2([],Y,Y).
rev2([H|T],A,Y) :- rev2(T,[H|A],Y).

% (***** Wffs and thms *****)
:- op(450,xfy,[/\,\/]).              % conjunction, disjunction
:- op(500,xfx,[=>,==>]).             % implication, sequent symbol
:- op(400,fx,[~,#]).                 % negation, box

/* minimal syntax check for input goal
 *
 * seq ::= formlist ==> formlist (list usual Prolog syntax)
 * form ::= atom | ~ form | # form | form => form | form \/ form | form /\ form
 *                   (atom is just Prolog atom; too generous, really)
 */

seq_syntax(X):- var(X),write('Prolog vars not allowed in sequent'),!,fail.
seq_syntax(WffList ==> WffList2) :-
	wfflist_syntax(WffList),
        wfflist_syntax(WffList2), !.
seq_syntax(_) :- write('Not correct sequent syntax'),nl,fail.
wfflist_syntax(X):- var(X),write('Prolog vars not allowed in wfflist'),!,fail.
wfflist_syntax([]).
wfflist_syntax([Wff|Rest]) :- wff_syntax(Wff), !, wfflist_syntax(Rest).
wfflist_syntax(_) :- write('Not correct wff list syntax'),nl,fail.
wff_syntax(X):- var(X),write('Prolog vars not allowed in wff'),!,fail.
wff_syntax(A=>B) :- !,wff_syntax(A),wff_syntax(B).
wff_syntax(A/\B) :- !,wff_syntax(A),wff_syntax(B).
wff_syntax(A\/B) :- !,wff_syntax(A),wff_syntax(B).
wff_syntax(~ A) :- !,wff_syntax(A).
wff_syntax(# A) :- !,wff_syntax(A).
wff_syntax( X) :- atomic(X), !.
wff_syntax(X) :- write('Not correct wff syntax: '),write(X), nl,fail.

%  inference rules:
%  rule( Name, [OldSeq, incomplete], [OldSeq, Name], NewSeqs )
%
%  Name: rule with parameter identifying by number formula rule applies to
%  OldSeq: sequent rule applies to
%  NewSeqs: list of 0,1 or 2 objects each of form [Seq,incomplete]
%      these are the subgoals generated by applying the rule backwards
%

    
/* axiom relabels sequent as axiom, if it is                           

   Axiom      : -------------
                 [..a..] |- [..a..]                                         */

rule(axiom,[Antes ==> Concs,incomplete],[Antes ==> Concs,axiom],[]) :-
         member(X,Concs),member(X,Antes).

/* the inference rules


                     L |- [..a..]   L |- [..b..]
   &-Introduction: --------------------
                     L |- [.. a & b..]                             */

rule(andI(R),[Antes ==> Concs,incomplete],
          [Antes ==> Concs, andI(R)],
          [ [Antes ==> NewConcs1,incomplete], 
            [Antes ==> NewConcs2,incomplete] ] )  :-
         replace_list(Concs,R,A/\B,[A],NewConcs1),
         replace_list(Concs,R,A/\B,[B],NewConcs2).
         
/*                    .. A,B..|- C
   &-Elimination : --------------
                      .. A/\B..|- C
   for mth hypothesis of sequent                                 */

rule(andE(M),[Antes ==> C ,incomplete],
           [Antes ==> C, andE(M)],
          [ [NewAntes ==> C, incomplete] ] )  :-
           replace_list(Antes,M,A/\B,[A,B],NewAntes).

/* Or Introduction - 

                    L |- [..a,b..]
                   --------
                    L |- [..a v b..]                                  */
      
rule(orI(R),[Antes ==> Concs,incomplete],
            [Antes ==> Concs, orI1(R)],
          [ [Antes ==> NewConcs,incomplete] ] )  :-
         replace_list(Concs,R,A\/B,[A,B],NewConcs).
         

/* Or elimination:   [..a..]|- c       [..b..]|- c
                     -----------------------------
                            [.. a v b ..] |- c                      */
         
rule(orE(M),[Antes ==> C,incomplete],
            [Antes ==> C, orE(M)],
            [ [NewAntes1 ==> C,incomplete], 
              [NewAntes2 ==> C,incomplete] ] )  :-
         replace_list(Antes,M,A\/B,[A],NewAntes1),
         replace_list(Antes,M,A\/B,[B],NewAntes2).


/*

				L u [a] |- [..b..]
   Implication Introduction : ----------------
				L |- [..a => b..]                   */
   


rule(impI(R),[Antes ==> Concs,incomplete],
             [Antes ==> Concs,impI(R)],
             [ [[A|Antes] ==> NewConcs ,incomplete] ] )  :-
               replace_list(Concs,R,A=>B,[B],NewConcs).         

/*

		   		 .... |- [a] u c    ..b.. |-  u
   Implication Elimination  : -----------------------------------
				    ..a=>b.. |- c         	            
   for the Mth hypothesis                                          */

rule(impE(R),[Antes ==> Concs,incomplete],
             [Antes ==> Concs, impE(R) ],
             [ [NewAntes1 ==> [A|Concs] ,incomplete], 
               [NewAntes2 ==> Concs,incomplete] ] )  :-
         replace_list(Antes,R,A=>B,[],NewAntes1), 
         replace_list(Antes,R,A=>B,[B],NewAntes2). 

/*
                         [..A..]|- [.. ..]
   Not intro:            -----------------
                         [.. ..]|- [..~A..]                   */

rule(notI(R),[Antes ==> Concs,incomplete],
             [Antes ==> Concs,notI(R) ],
             [ [[A|Antes] ==> NewConcs ,incomplete]]) :-
	       replace_list(Concs,R,~A,[],NewConcs).

/*
                         [.. ..] |- [..A ..]
   Not elim            -----------------------
                         [..~A..]|- [....]                   */

rule(notE(R),[Antes ==> Concs,incomplete],
               [Antes ==> Concs,notE(R) ],
             [ [NewAntes ==> [A|Concs] ,incomplete]]) :-
	        replace_list(Antes,R,~A,[],NewAntes).


/*  Box introduction
               boxes(L) |- a, boxes(M)
               -------------------
                 L |- # a, M                                        */

rule(boxI(R),[Antes ==> Concs, incomplete],
           [Antes ==> Concs,boxI(R)],
          [ [NewAntes ==> NewConcs ,incomplete] ] )  :-
	 nth_member(R,Concs, # _),
         boxes(Antes,NewAntes),
	 boxes(Concs,NewConcs).

/*  Box elimination

                 ...h ... |- ..a..
                ----------
                 ...#h... |- ..a..                       */

rule(boxE(M), [Antes ==> Concs,incomplete],
              [Antes ==> Concs,boxE(M)],
             [ [NewAntes ==> Concs, incomplete] ] ) :-
  replace_list(Antes,M,#H,[H],NewAntes).

/* boxes( +Forms, ?New )  returns list of F such that #F appears in Forms  */

boxes([],[]).
boxes([(# A)|Rest],[A|Rrest]) :- !, boxes(Rest,Rrest).
boxes([_|Rest],Rrest) :- boxes(Rest,Rrest).


/* replace_list(OldHyps,Number,OldHyp,NewHyps,NewHypList)
  in mode +,+,pattern,? replaces hyp with one or more new hyps;     
    reversible modes                                              */
  replace_list([],_,_,_,_) :- !,fail.
  replace_list([H|T],1,H,New,NewList) :- append(New,T,NewList).
  replace_list([H|T],N,X,New,[H|NewList]) :- var(N),!,  
                        replace_list(T,M,X,New,NewList),N is M+1.
  replace_list([H|T],N,X,New,[H|NewList]) :-  M is N-1,
                        replace_list(T,M,X,New,NewList).

/* nth_member(Number,List, NthMember)                             
   reversible modes,                                               */
  nth_member(_,[],_) :- !, fail.
  nth_member(1,[H|_],H).
  nth_member(N,[_|T],X) :- var(N), !, nth_member(M,T,X),N is M+1.
  nth_member(N,[_|T],X) :- M is N-1, nth_member(M,T,X).

/***** Printing wffs and thms *****/

printseq( [] ==> Concl ) :- write([]), write('==> '), write(Concl).
printseq( [H|T] ==> Concl ) :-  write('1: '), write(H), nl, print_a(T,2),
                            write('    ==> '), write(Concl).

print_a([],_).
print_a([H|T],N) :- write('  '), write(N), write(': '), write(H),
                    nl, NN is N+1, print_a(T,NN).
  

/***** Read sequent goal from file  ****/

/* file should contain sequent, terminated by full stop, eg

   [a,b/\c,#d] ==> [d].

   read_goal( +Filename, -Goal )
     supply filename, will instantiate Goal to der( [ Seq, incomplete ] ),
     where Seq is the sequent in file with name Filename.
   
*/

read_goal( Filename, der([Goal, incomplete]) ) :-
    see(Filename),
    (   (read( Goal ), seq_syntax( Goal ))
            ->	seen
       ; write( 'problem reading in file ' ), write(Filename), nl, seen, fail
    ).


/* complete( Der ) test whether Der is a complete derivation
 * assuming derivation format above.
 */
 
complete( der( [_, axiom], [] ) ) :- !.
complete( der( [_,_], [] ) ) :- !, fail.
complete( der( _, Ders ) ) :- complete_list(Ders).
complete_list( [] ).
complete_list( [D|Ders] ) :- complete(D), complete_list(Ders).


/* print_proof(P) attempts pretty printing of proof
 *  assumed to be a term der(_,_) structured as above.
 * Use indenting to represent subgoals
 */

print_der( D ) :- indent_der( 0, D ), !, nl,
	          ( complete(D) -> write( 'Derivation complete' )
		    ; true ),
		  nl,nl.

indent_der( N, der(Node,Subs) ) :-
       0 =< N,
       indent_node( N, Node ),
       M is N+1,
       indent_ders( M, Subs ).

indent_ders( _, [] ).
indent_ders( M, [H|T] ) :-
	indent_der( M, H),
	indent_ders( M, T ).

indent_node( N, [ L ==> Concl, Rule ] ) :-
    indent_numbered( N, 1, Rule, L ==> Concl ).

indent_numbered( N, M, Rule, [H|T] ==> Concl ) :-
	indent(N), write(' '),write(M),write(': '),
	write(H),nl, MM is M+1, indent_numbered(N,MM,Rule,T ==> Concl).
indent_numbered( N, _, Rule, [] ==> Concl ) :-
	indent(N), write(' ==> '), write(Concl), nl,
	indent(N), write(' Rule: '), write( Rule ), nl.
indent(0).
indent(N) :- 0< N, write('-'), M is N-1, indent(M).

test( der( [ [a] ==> a /\ a, and1(1)],
	     [ der( [[a] ==> [a], axiom ], [] ),
                       der( [[a] ==> [a], axiom ], [] )
	     ] ) ).

