% Intuitionistic theorem prover
% Written by Roy Dyckhoff, Summer 1991    
% Modified to use the LWB syntax  Summer 1997
% and simplified in various ways...

% runs under SICSTUS Prolog
% for other Prologs, maybe a different way of timing is required
% and maybe "append" needs to be defined explicitly.

% Incorporates the Vorob'ev-Hudelmaier etc calculus (I call it LJT)
% See RD's paper in JSL 1992:
% "Contraction-free calculi for intuitionistic logic"

% Torkel Franzen (at SICS) gave me good ideas about how to write this 
% properly, taking account of first-argument indexing

% and I learnt a trick or two from Neil Tennant's "Autologic" book.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% A is formula to prove
% TIme is in millisec

time( A,  Time ) :-
    statistics(runtime, _),
    prove(A,Result),
    statistics(runtime, [ _, Time]),
    write(Result), 
    nl. 

prove( A,true ) :- 
    provable(A), !.
prove( _,false ). 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% SYNTAX
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Use of LWB concrete syntax from June 97
% provided that one uses bracketmode "full"

:- op(425,  fy,  ~ ).
:- op(450, yfx,  & ).    % left associative
:- op(450, yfx,  v ).    % left associative
:- op(500, xfx,  <-> ).  % non associative
:- op(500, xfy,  ->).    % right associative  
                %%% WARNING, this overwrites Prolog's ->


% e.g.  formulae look like  ((a & b ) -> c) -> false, ~(~( a v (~a)))
% where a,b,c etc are atoms

% all atoms MUST be of form pv(X) for some X

% inspv(A, NewA) ensures that NewA has all the atoms with pv/1 as an 
% explicit constructor, making the clauses more deterministic
% it also eliminates definitions of <-> and ~.

inspv( A v B, A1 v B1) :- !, 
  inspv(A, A1), inspv(B, B1).
inspv( A & B, A1 & B1) :- !, 
  inspv(A, A1), inspv(B, B1).
inspv( A -> B, A1 -> B1) :- !, 
  inspv(A, A1), inspv(B, B1).
inspv( A<->B, (A1->B1)&(B1->A1) ) :- !,   % removes definition of <->
  inspv(A, A1), inspv(B, B1).
inspv( ~A , A1->false ) :- !,       % removes definitions of negation
  inspv(A, A1).
inspv( true, true ) :- !.           % true not an atom 
inspv( false, false ) :- !.         % false not an atom 

inspv( A, pv(A) ).                  % when all else fails 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% UTILITIES
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% AtomImps is an ordered list PL of pairs (A,LA) where LA is a list
% and A is an atom
% lists PL are ordered by @< relation on first conponent
% LA is list of formulae B 
% No attempt to avoid repetition in LA.

% meaning( []) = true
% meaning( ( Pair | Rest|) = meaning( Pair) & meaning(Rest)
% meaning( (A,Bs) ) = A -> conjunction(Bs)

% extract( AtomImps, A,  Bs, RestImps)
% called with AtomImps and A known (an Atom); returns Bs and RestImps
% thus  meaning(AtomImps) ==  meaning(A->Bs) & meaning(RestImps)

extract( [ ], _, [], []).
extract( [  Pair | AtomImps], A,  Bs, [ Pair | RestImps ] ) :- 
  Pair = (A1, _), 
  A @> A1,                                    % still worth looking
  extract(AtomImps, A, Bs, RestImps). 
extract( [ Pair | RestImps], A,  Bs, RestImps) :-
  Pair = (A, Bs).                             % Found it
extract( AtomImps, A,  Bs, AtomImps) :-
  AtomImps = [ (A1, _) | _ ],  
  A @< A1,                                    % gone too far
  Bs = [].                           % Not there, return empty list

% insert( AtomImps, A -> B, AtomImps1)
% where A is an atom

insert( [], A -> B,  [ (A, [B]) ] ).
insert( [  Pair  |AtomImps], A -> B, [ Pair | AtomImps2 ] ) :-
   Pair = (A1, _), 
   A @> A1,   % Needs to go further in
   insert(AtomImps, A -> B, AtomImps2).
insert( [ (A, Bs)|AtomImps], A -> B, [(A,[B|Bs])|AtomImps] ).  % Here!
insert( [ Pair   |AtomImps], A -> B, [(A,[B]),Pair|AtomImps] ) :-
   Pair = (A1, _), 
   A @< A1.   % Needs to go before Pair

% ===============================

heuristics(on).  % change this to switch heuristics off...


order(  NestImps, _, _,  NestImps ) :- 
  heuristics(off). 

order(  NestImps, G, AtomImps,  NewNestImps ) :- 
  heuristics(on), 
  order0(  NestImps, G, AtomImps, [], NewNestImps).

order0( [], G, AtomImps, Bads, Bads1 ) :-
  order1(Bads, G, AtomImps, [], Bads1).

order0( [ A | In], G, AtomImps, Bads,  [ A | Out] ) :-
  good_for(A, G), 
  !, 
  order0( In, G, AtomImps, Bads , Out ).

order0( [ A | In], G, AtomImps, Bads,  Out ) :-
  % not so good_for(A, G),
  order0( In, G, AtomImps, [ A | Bads], Out ).

good_for(_ -> false, _).
good_for(_ -> G, G).


order1( [], _, _, NewBads, NewBads ).

order1( [ A | In], G, AtomImps, NewBads, [ A | Out] ) :-
  nice_for(A, G, AtomImps), 
  !,
  order1(In, G, AtomImps, NewBads, Out).

order1( [ A | In], G, AtomImps, NewBads,  Out ) :-
  % not so nice_for(A, G, AtomImps),
  order1( In, G, AtomImps, [ A | NewBads], Out ).

nice_for( _ -> pv(B) , G, AtomImps) :-
  on( (pv(B), Bs), AtomImps), 
  !, % no need to see if pv(B) is in NestImps in any other way
  (on( G, Bs); on(false, Bs)),
  !.

% ===============================

% select(List, Element, Remainder)
% ALL the backtracking is done here....

select( [X | L], X,  L).
select( [Y | L], X,  [Y | M]) :- 
  select(L,X, M).


on( A, [ A | _ ] ).
on( A, [ _ | Rest] ) :- on(A, Rest).

on1( A, L ) :-
   on(A, L),
  !.

on3( A, L, Res ) :-
  on1(A, L),
  !, 
  Res = true.
on3(_, _, false).
 
/*
append( [], L, L ).
append( [ H | T], L, [ H | TL] ) :-
	append(T, L, TL).

*/

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% MAIN PROGRAM
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% ==============================
provable( A ) :-    
  inspv(A, A1), 
  redant1(A1 -> false, [], [], [], [], false),   % check classical provability
  redsucc(A1, [], [], []), !.

% ==============================
 

% AtomImps is a list as described above
% NestImps is a list of formulae of the form (C->D)->B
% where if B = false, then D=false
% Atoms is a list of atoms

redant( [ ], AtomImps, NestImps, Atoms,  G) :-
  redsucc(G, AtomImps, NestImps, Atoms).
redant( [ A | L], AtomImps, NestImps, Atoms, G) :-  
  redant1(A, L, AtomImps, NestImps, Atoms, G).

% ------------------------------

redant1(  pv(A), _, _, _, _, pv(A)  ).

redant1( pv(A),  L, AtomImps, NestImps, Atoms, G) :- 
   \+ G = pv(A) ,
  extract(AtomImps, pv(A), Bs, RestAtomImps), 
  append(Bs, L, BsL), 
  redant( BsL, RestAtomImps, NestImps, [pv(A)|Atoms], G ).

redant1( true, L, AtomImps, NestImps, Atoms, G ) :- 
  redant( L, AtomImps, NestImps, Atoms, G).

redant1( false, _, _, _, _, _ ).

redant1( A & B, L, AtomImps, NestImps, Atoms, G ) :- 
  redant1(A, [B | L], AtomImps, NestImps, Atoms, G).

redant1( A v B, L, AtomImps, NestImps, Atoms, G ) :- 
  redant1( A, L, AtomImps, NestImps, Atoms,  G),
  redant1( B, L, AtomImps, NestImps, Atoms,  G).

redant1( A -> B, L, AtomImps, NestImps, Atoms, G ) :-
  redantimp(A, B, L, AtomImps, NestImps, Atoms, G). 


% ------------------------------
% redantimp

redantimp( pv(A), B, L, AtomImps, NestImps, Atoms, G ) :-
  redantimpatom( pv(A), B, L, AtomImps, NestImps, Atoms, G).

redantimp( true, B, L, AtomImps, NestImps, Atoms, G ) :- 
  redant1(B, L, AtomImps, NestImps, Atoms, G).

redantimp( false, _, L, AtomImps, NestImps, Atoms, G ) :- 
  redant( L, AtomImps, NestImps, Atoms, G).

redantimp( C & D, B, L, AtomImps, NestImps, Atoms,  G ) :-  
  redantimp(C, (D -> B), L, AtomImps, NestImps, Atoms, G).

redantimp( C v D, B, L, AtomImps, NestImps, Atoms,  G ) :-
  redantimp(C, B, [ (D -> B) | L ], AtomImps, NestImps, Atoms, G).

redantimp( C -> D, B, L, AtomImps, NestImps, Atoms,  G ) :-
  redantimpimp( C, D, B, L, AtomImps, NestImps, Atoms, G).

% ------------------------------
% redantimpimp 

redantimpimp( C, false, false, L, AtomImps, NestImps, Atoms, G ) :- 
  redant(L, AtomImps, [ (C -> false) -> false | NestImps ], Atoms, G).

    % next clause exploits ~(C->D) eq  (~~C & ~D)
    % which isn't helpful when D = false

redantimpimp( C, D, false, L, AtomImps, NestImps, Atoms, G) :-
  \+(D = false),  
  redantimpimp( C, false, false,  [ D -> false | L] , AtomImps, NestImps, Atoms, G).

redantimpimp( C, D, B, L, AtomImps, NestImps, Atoms, G) :- 
  \+ (B = false), 
  redant(L, AtomImps, [ (C -> D) -> B | NestImps ], Atoms, G).

%-----------------------------------------------
%redantimpatom

redantimpatom( A, B, L, AtomImps, NestImps, Atoms, G ) :-
  on3(A, Atoms, Res), 
  redantimpatomres(Res,  A, B, L, AtomImps, NestImps, Atoms, G ).

redantimpatomres( true, _, B, L, AtomImps, NestImps, Atoms, G ) :- 
  % A is on Atoms: reduce using rule ->L1
  redant1(B, L, AtomImps, NestImps, Atoms, G).

redantimpatomres( false,  A, B, L, AtomImps, NestImps, Atoms, G ) :-
  % A is atom but not on Atoms, add A->B to AtomImps
  insert(AtomImps, A -> B, AtomImps1), 
  redant(L, AtomImps1, NestImps, Atoms, G).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% redsucc(Goal, AtomImps, NestImps, Atoms)

% All conjunctions or disjunctions on the left 
% have been reduced before 'redsucc' is called

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

redsucc( true, _, _, _  ).

redsucc( false, AtomImps, NestImps, Atoms ) :- 
     % we could now use a classical decision procedure, but 
     % present data structures are organised differently...
  inconsis( AtomImps, NestImps, Atoms).

redsucc( pv(A), AtomImps, NestImps, Atoms ) :- 
  on3(pv(A), Atoms,  Res),
  redsuccpv(Res,  pv(A), AtomImps, NestImps, Atoms).

redsuccpv( true, _, _, _, _ ).
redsuccpv(false,  pv(A), AtomImps, NestImps, Atoms ) :-
  posin(pv(A), AtomImps, NestImps),                     % MAJOR PRUNING HERE
  redsucc_choice( pv(A), AtomImps, NestImps, Atoms).

redsucc( A & B, AtomImps, NestImps, Atoms ) :- 
  redsucc(A, AtomImps, NestImps, Atoms),
  redsucc(B, AtomImps, NestImps, Atoms).

  % next clause deals with succedent (A v B) by pushing the
  % non-determinism into the treatment of implication on the left
  % note trick for creating a new variable

redsucc( A v B, AtomImps, NestImps, Atoms ) :- 
  P = pv( (AtomImps, NestImps, Atoms) ),
  redant( [ A -> P, B -> P ], AtomImps, NestImps, Atoms, P). 

redsucc( A -> B, AtomImps, NestImps, Atoms ) :-
  redant1(A, [], AtomImps, NestImps, Atoms, B).

%----------------------------------------

% Now we have the hard part; maybe lots of formulae 
% of form (C->D)->B  in Imps to choose from!
% Which one to take first? We need some heuristics:
% first we take those where the minor premiss is trivial;
% next we take those where B is an atom and B->G is in AtomImps
% next we try to choose B a disjunction (even if G isn't)
% finally we choose the others

redsucc_choice( G, AtomImps, NestImps, Atoms ) :- 
  order(NestImps, G, AtomImps,  OrdImps),
  select(OrdImps, ( (C->D) -> B), Rest),
  redant3(C, D, B, AtomImps, Rest, Atoms, G),
  !.  % MAIN CUT here

redant3( C, D, B, AtomImps, NestImps, Atoms, G ) :-
  redant1(D->B, [], AtomImps, NestImps, Atoms, C->D), %  Left Premiss
  !,  % CUT here; rule is semi-invertible
   redant1(B, [], AtomImps, NestImps, Atoms, G).            % Right Premiss

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Pruning utilities

posin( G, AtomImps, NestImps ) :-
  % G occurs strictly positively on LHS
  posin1( AtomImps, G ), 
  ! ;
  posin2( NestImps, G ). 

posin1( [ ( _, Bs ) | AtomImps ], G ) :-
  posin2( Bs, G ), 
  ! ; 
  posin1( AtomImps, G ).
  
posin2( [ B | Bs ], G ) :-
  posin3( B,G ), 
  ! ;
  posin2( Bs, G).

posin3( A v B,G ) :-
  posin3(A,G), 
  posin3(B,G).

posin3( A & B,G ) :-
  posin3(A,G), 
  ! ;
  posin3(B,G).

posin3( _ -> B, G ) :-
  posin3(B,G).
 
posin3( false, _ ).
posin3( G, G ).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Classical ATP utility

% from now on, goal is always = false...

inconsis( AtomImps, [ (C->D)->B |  Rest], Atoms ) :-  
  inconsis1(B, AtomImps, Rest, Atoms, C, D).

inconsis1( false, AtomImps, NestImps, Atoms, C, _  ) :- 
    % _ = false by construction, so can be ignored.
    % uses ((( C -> false) -> false) -> false) eq (C -> false)
  redant1( C, [], AtomImps, NestImps, Atoms, false).  

inconsis1( B, AtomImps, NestImps, Atoms, C, D ) :- 
  \+ B = false,  % so can exploit ~((C->D)->B) eq  ~~(C->D) & ~B
  redantimpimp( C, D, false, [], AtomImps, NestImps, Atoms, false ), 
  redant1( B, [], AtomImps, NestImps, Atoms, false ).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% END
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%