################################################# 
#################################################
################################################# 
9 Appendix: LWB and Prolog code to generate formulae 
#################################################
################################################# 
#################################################

#################################################
#################################################
# 9.0 General utilities 
#################################################
# for the LWB 
# Don't forget to include these if needed 

proc : p(i) 
  # takes an integer > 0, returns an atom 
  # eg from 123 it returns p123 
begin 
  return symbol("p", i); 
end; 

#------------------------------------------------
# Here is how to test some problems:
# modify this appropriately...
for j := 1 to 8 do
     begin
        ct :== clockticks();  # :== is silent
        provable(class_n(j)); 
        clockticks() - ct;
     end;
%================================================
% for Prolog
% Prolog operator definitions
:- op(425,  fy,  ~ ).
:- op(450, yfx,  &).    % left associative
:- op(475, yfx,  v ).    % left associative
:- op(500, xfx,  <-> ).  % non associative
:- op(500, xfy,  ->).    % right associative  
      %%% WARNING, this overwrites Prolog's ->

% Timing tools differ between implementations...

#################################################
#################################################
# 9.1 de Bruijn formulae
#################################################
load(ipc);
proc : de_bruijn_p(n)
  # generates the 2n+1^th "de Bruijn" formula
  # should be provable
  local a, c, i, last;
begin
  c := p(1);
  last := 2 mult n+1;
  for i := 2 to last do c := c & p(i) ; 
  a := true; 
  for  i := 1 to last-1  do 
     a := a & ((p(i) <-> p(i+1)) -> c);
  a := a & ((p(last) <-> p(1)) -> c);  
  return ( a -> c );
end; #de_bruijn_p 

proc : de_bruijn_n(n)
  # generates the 2n^th "de Bruijn" formula
  # should be not provable
  # tweaked to make them classically provable...
  local a, c, i, last;
begin
  c := p(1); 
  last := 2 mult n;
  for i := 2 to last do c := c & p(i) ; 
  a := true; 
  for  i := 1 to last-1  do 
     a := a & ((p(i) <-> p(i+1)) -> c);
  a := a & ((p(last) <-> p(1)) -> c);  
  return ( a -> ( p(0) v c v ~p(0) ));
end; #de_bruijn_n

%Prolog code--------------------------------------
de_bruijn_p(N, F ) :-
  N1 is 2*N + 1,
  dB(N1, F).
de_bruijn_n(N, F ) :-
  N1 is 2*N,
  dB(N1, A -> C),
  F = A -> ( p0 v C v ~p0 ).
dB(N, A -> C) :-
  atoms(N, N, [], Ps),
  conj(Ps, C),
  make(Ps, C, As),
  conj(As, A).

atoms(_, M, Atoms, Atoms) :- M =< 0.
atoms(N, M, Atoms, Result) :-
  M > 0,
  M1 is M-1,
  atoms(N, M1, [p(M) | Atoms], Result).

conj( [H], H).
conj( [H1, H2 | Tail], C) :-
  conj( [H1 & H2 | Tail], C).

make([ P0 | Ps], C, As ) :-
  make4([ P0 | Ps], P0, C, As). 
make4( [Pn], P0, C, [(Pn<->P0)->C] ).
make4( [P1, P2 | Tail], P0, C, [(P1<->P2)->C | Rest] ) :-
  make4( [P2 | Tail], P0, C, Rest).

#################################################
#################################################
#9.2 Pigeonhole formulae
#################################################
load(ipc);
proc : ph_p(n)
begin
  return ( left(n) -> right(n) );
end; # ph_p 

proc : ph_n(n)
begin
  return ( left_n(n) -> right(n) );
end; # ph_p 

proc : conjoin( c1, c2)
begin
  if c1 = true then return c2 ; else return c1 & c2;
end; #conjoin

proc : disjoin( d1, d2 ) 
begin
  if d1 = false then return d2 ; else return d1 v d2;
end; # disjoin

proc : right(n)
  local d, h, p1, p2 ;
begin
  d := false;
  for h := 1 to n do
    for p1 := 1 to n+1 do
      for p2 := p1+1 to n+1 do
        d := disjoin(d, (o(p1, h) & o(p2, h))) ;
  return d;
end; # right

proc : left(n)
  local c, d, p, h;
begin
  c := true;
  for p := 1 to n+1 do
    begin
      d := false;
      for h := 1 to n do
        d := disjoin(d, o(p,h) );
      c := conjoin(c,d);
    end;
  return c;
end; # left

proc : left_n(n)
# uses DN to make non-provable
  local c, d, p, h, oph;
begin
  c := true;
  for p := 1 to n+1 do
    begin
       d := false;    
       for h := 1 to n do
         begin
           oph := o(p,h);
           if h = n then oph := ~ ~oph;   
           d := disjoin(d, oph); 
         end; 
       c := conjoin(c,d); 
    end;
  return c;
end; # left_n

%Prolog code--------------------------------------
ph_p(N, L -> R ) :-
  left(N, pos, L),
  right(N,R).

ph_n(N, L -> R ) :-
  left(N, neg, L),
  right(N,R).

right(N, R) :-
  disj(N, 1, false, R).

disj( N, H, D, D ) :-
  H > N.
disj( N, H, D, D1 ) :-
  H =< N,  
  N1 is N+1, 
  disj1(N1, H, 1, D, D0),
  H1 is H+1, 
  disj(N, H1, D0, D1).

disj1( N1, _, P1, D, D ) :- 
  P1 > N1.
disj1( N1, H, P1, D, D1 ) :- 
  P1 =< N1,
  P11 is P1 + 1,
  disj2(N1, H, P1, P11, D, D0),
  disj1(N1, H, P11, D0, D1).

disj2( N1, _, _, P2, D, D ) :-  
  P2 > N1.
disj2( N1, H, P1, P2, D, D1 ) :-
  P2 =< N1,
  P21 is P2+1, 
  disjoin(D, o(P1,H) & o(P2,H), DC), 
  disj2(N1, H, P1, P21, DC, D1).
  
left( N, Sign, L ) :-
  N1 is N+1, 
  conj(N1, N, 1, Sign, true, L).

conj(N1, _, P, _, C, C ) :- 
  P > N1.
conj(N1, N, P, Sign, C, C1 ) :-
  P =< N1,
  cd(N, 1, P, false, Sign, D),
  P1 is P+1, 
  conjoin(C, D, CD), 
  conj(N1, N, P1, Sign, CD, C1).

cd( N, H, _, D,  _,  D )  :-  
  H > N.
cd( N, H, P, D, Sign, D1 ) :-
  H =< N,
  H1 is H+1,
  signify(Sign, o(P,H), H-N,  SOPH), 
  disjoin(D, SOPH, DOPH), 
  cd(N, H1, P, DOPH, Sign, D1).
  
signify( neg, X,  H - H, ~ ~X) :- !. 
signify( _, X, _ - _, X). 
disjoin(false, D, D) :- !.
disjoin(D1, D, D1 v D).
conjoin(true, D, D) :- !.
conjoin(D1, D, D1 & D).

#################################################
#################################################
9.3	
#################################################
# Examples of Franzen
# con_p(n) requires n contractions in LJ
# con_n(n) similar but unprovable
#################################################
load(ipc);

proc : nix( a )
begin
  return ( a -> f) ;  
end; # nix
# like negation, but to avoid use of Glivenko's theorem

proc : trans_e(n)
  # n >= 1
  local d, i;
begin
  d := nix(p(1)) ;
  for i := 2 to n do d := d v nix(p(i));
  return d;
end; #trans_e

proc : trans_en(n)
  # n >= 1
  local d, i;
begin
  d := ~ ~nix(p(1)) ;
  for i := 2 to n do d := d v nix(p(i));
  return d;
end; #trans_e

proc : trans_a(n)
  # n >= 1
  local c, i;
begin
  c := p(1) ;
  for i := 2 to n do c := c & p(i);
  return c;
end; #trans_a

proc : con_p( n )
  # n >= 0
begin
  return (nix (nix (trans_a(n) v trans_e(n)))); 
end; # con_p

proc : con_n( n )
  # n >= 1
begin
  return (nix (nix (trans_a(n) v trans_en(n)))); 
end; # con_n

%Prolog code--------------------------------------

con_p(N, ( (C v D) -> f) -> f ) :-
   disjs(N, pos, D),
   conjs(N, C). 
con_n(N, ( (C v D) -> f) -> f ) :-
   disjs(N, neg, D),
   conjs(N, C). 

conjs(1, p(1)).
conjs(N,  C & p(N) ) :-
  N > 1,
  N1 is N-1, 
  conjs(N1, C).

disjs(1, pos, p(1) -> f).
disjs(1, neg, ( ~ ~p(1)) -> f).
disjs(N,  Sign, D v ( p(N) -> f)  ) :-
  N > 1,
  N1 is N-1, 
  disjs(N1, Sign, D).

#################################################
#################################################
9.4	
#################################################
# Schwichtenberg's formulae
# normal natural deduction of schwicht_p(n) has size exponential in n
% easy for sequent calculus-based systems
#################################################
load(ipc);

proc : schwicht_p( n ) 
   # n >= 0
  local ant, i;
begin
  ant := p(n);
  for i:= 1 to n do
    ant := ant & ( p(i) -> p(i) -> p(i-1));
  return (ant -> p(0) );
end; #schwicht_p
proc : schwicht_n( n ) 
   # n >= 0
  local ant, i;
begin
  ant := ~ ~p(n);
  for i:= 1 to n do
    ant := ant & ( p(i) -> p(i) -> p(i-1));
  return (ant -> p(0)) ;
end; #schwicht_n

%Prolog code------------------------------------------------

schwicht_p( N, A -> p(0) ) :-
  ant(N, 1, p(N), A).
schwicht_n( N, A -> p(0) ) :-
  ant(N, 1, ~ ~p(N), A).
ant( N, I, A, A ) :- I > N.
ant( N, I, A, A1 ) :- 
  I =< N,
  I1 is I+1, IM1 is I-1, 
  ant(N, I1, A & ( p(I) -> p(I) -> p(IM1)) , A1).
#################################################
#################################################
9.5	
#################################################
# Korn & Kreitz's formulae
# modified to avoid use of Glivenko theorem
#################################################
load(ipc);
proc : nix( a )
# like negation, but to avoid use of Glivenko's theorem
begin
  return ( a -> f) ;  
end; # nix
proc : kk_p( n ) 
   # n >= 1
  local lhs, lhsr, i;
begin
  lhs := nix(a(0)) & ((b(n)->b(0))->a(n));
  for i := 1 to n do
    lhs := lhs & ((b(i-1)->a(i))->a(i-1));
  lhsr  := ((b(n)->b(0))->a(n)) & nix(a(0));
  for i := 1 to n do
   lhsr := ((b(i-1)->a(i))->a(i-1)) & lhsr ;
  return( nix(lhs) & nix(lhsr) );  
end; #kk_p


proc : kk_n( n ) 
   # n >= 1
   # use of double negation to 
	  #   maintain classical provability but 
   #   destroy intuitionistic provability
  local lhs, i;
begin
  lhs := nix(a(0)) & ((~ ~b(n)->b(0))->a(n));
  for i := 1 to n do
    lhs := lhs & ((~ ~b(i-1)->a(i))->a(i-1));
  return( nix(lhs));  
end; #kk_n

%Prolog code--------------------------------------

kk_p(N, (A->f) & (AR->f) ) :- kk_p(N, N, A), kkr(N,N,AR).
kk_p(N, 0,  (a(0) -> f) & ((b(N)->b(0))-> ( a(N)) ) ).
kk_p(N, I, LHS & ((b(I1)->a(I))->( a(I1))) ) :-
  0 < I, 
  I1 is I-1,
  kk_p(N, I1, LHS).

kkr(N, 0,  ((b(N)->b(0))->  a(N) )  & (a(0) -> f)  ).
kkr(N, I,  ((b(I1)->a(I))->  a(I1) )  & LHS ) :-
  0 < I, 
  I1 is I-1,
  kkr(N, I1, LHS).

kk_n(N, A -> f ) :- kk_n(N, N, A).
kk_n(N, 0,  (a(0) -> f) & ((~ ~b(N)->b(0))-> ( a(N)) ) ).
kk_n(N, I, LHS & ((~ ~b(I1)->a(I))->( a(I1))) ) :-
  0 < I, 
  I1 is I-1,
  kk_n(N, I1, LHS).

#################################################
#################################################
# 9.6 Equivalences
#################################################

proc : equiv_p(n) 
  # n >= 1
  local l, r, i ;
  begin
    l := a(1); r := a(1);
    for i := 2 to n do 
      begin
        l := l <-> a(i);
        r := a(i) <-> r ; 
      end;
   return ( l <-> r);  
  end; #equiv_p

proc : equiv_n(n) 
  # n >= 1
  local l, r, i ;
  begin
    l := ~ ~a(1); r := a(1);
    for i := 2 to n do 
      begin
        l := l <-> a(i);
        r := a(i) <-> r ; 
      end;
   return ( l <-> r);  
  end; #equiv_n

%Prolog code--------------------------------------
equiv_p( N, A ) :- equiv( N, p, A).
equiv_n( N, A ) :- equiv( N, n, A).
equiv( 1, n,  (~ ~a(1)) <-> a(1) ).
equiv( 1, p,  a(1) <-> a(1) ).
equiv(N, S, AB <-> BA ) :- 
   N > 1,
   N1 is N-1,  AN = a(N),
  equiv( N1, S, A1 <-> A2), 
  AB = A1 <-> AN, 
  BA = AN <-> A2.
#################################################
#################################################
#################################################
#################################################
#################################################
#################################################
#################################################