% Theorem prover for propositional Dummett logic LC
% i.e. Intuitionistic logic plus (A->B)v(B->A)

% Written by Roy Dyckhoff, Summer 1998    

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

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

% and Avellone, Ferrari and Miglioli (in Milano)
%  Technical Report in 1997 on duplication-free sequent calculi
%	for various intermediate logics
% and a paper by RD on making all the rules invertible. 

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

% 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
% provided that one uses bracketmode "full"

:- op(425,  fx,  ~ ).
:- 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 (for internal use) be converted to the 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 instances 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 instance of <->
  inspv(A, A1), inspv(B, B1).
inspv( ~A , A1->false ) :- !,       % removes instance 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 


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

% select(List, Element, Remainder)

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

on( A, [ A | _ ] ).
on( A, [ _ | Rest] ) :- on(A, Rest).
 
/*
append( [], L, L ).
append( [ H | T], L, [ H | TL] ) :-
        append(T, L, TL).

*/

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

% ==============================
provable( A ) :-    
  inspv(A, A1), 
  mkempty(Left),
  mkempty(Right),
  add(A1, Right, NewRight),  
  reduce( Left, NewRight ).

reduce( Left, Right ) :-
  get(Left, A, NewLeft),
  reduce1(A, NewLeft, Right ).

reduce( Left, Right ) :-
  reduced(Left),  % avoids a cut in clause 1 for reduce/2
  get(Right, A, NewRight),
  reduce2(A, Left, NewRight).

reduce( Left, Right ) :-
  reduced(Left),  % avoids cuts in clauses 1,2 for reduce/2
  reduced(Right),
  get_imps(Right, RImps),
  forall(select(RImps, A->B, RestImps), 
           reduce1(A, Left, ([], RestImps, [B])) 
        ).


% Left Rules ==========================
reduce1( pv(X), _, Right) :-
  on_atom(X, Right), 
  !.

reduce1( pv(X), Left, Right ) :-
  % not on_atom(X, Right),
  get_atom_imps(Left, X, B, Left1),
  add(B, Left1, Left2),
  add_atom(X, Left2, NewLeft), 
  reduce(NewLeft, Right).

reduce1( false, _, _).
reduce1( true, Left, Right) :-
  reduce(Left, Right). 

reduce1( A v B, Left, Right) :-
  reduce1(A, Left, Right),
  reduce1(B, Left, Right).

reduce1(A & B, Left, Right) :-
  add(B, Left, BLeft), 
  reduce1(A, BLeft, Right).

reduce1( false -> _ , Left, Right) :-
  reduce(Left, Right).

reduce1( true -> B, Left, Right) :-
  reduce1(B, Left, Right).

reduce1((C v D)->B, Left, Right ) :-
  add(D->B, Left, DBLeft), 
  reduce1(C->B, DBLeft, Right).

reduce1((C & D)->B, Left, Right ) :-
  reduce1(C->(D->B), Left, Right).

reduce1((C->D)->B, Left, Right ) :-
  add(C->D, Right, CDRight), 
  reduce1( D->B,  Left, CDRight),
  reduce1( B, Left, Right).

reduce1( pv(X) -> B, Left, Right) :-
  on_atom(X, Left),
  !, 
  reduce1(B, Left, Right).

reduce1( pv(X) -> B, Left, Right) :-
  % not on_atom(X, Left),
  add_atom_imp(X, B, Left, XBLeft),
  reduce(XBLeft, Right).

% Right Rules =========================

reduce2(pv(X), Left, _ ) :-
  on_atom(X, Left),
  !.

reduce2(pv(X), Left, Right ) :-
  % not on_atom(X, Left)
  add_atom(X, Right, XRight),
  reduce( Left, XRight).

reduce2( false, Left, Right) :-
  reduce(Left, Right).

reduce2(true, _, _).

reduce2(A & B, Left, Right ) :-
  reduce2(A, Left, Right),
  reduce2(B, Left, Right).

reduce2(A v B, Left, Right ) :-
  add(B, Right, BRight),
  reduce2(A, Left, BRight).

reduce2(A->B, Left, Right ) :-
  add_imp(A->B, Right, ABRight),
  reduce(Left, ABRight). 


% UTILITIES
%=================

% Sequents are represented by the pairs Left, Right
 % Left is a triple (Atoms, AtomImps, Ant)
  % Atoms is a list (unsorted) of terms X
  % AtomsImps is a sorted list of pairs (X,B)
  % Ant is the list of unprocessed formulae
 % Right is a triple (Atoms, Imps, Succ)
  % Atoms is a list (unsorted) of terms X
  % Imps is a list (unsorted) of implications A->B
  % Ant is the list of unprocessed formulae

% constructors
mkempty( ([], [], []) ).
add(A, (Atoms, Imps, Rest), (Atoms, Imps, [A | Rest]) ). 
add_atom(X, (LAtoms, LAImps, Ant), ( [X | LAtoms], LAImps, Ant)).
add_atom_imp(X, B, (LAtoms, LAImps, Ant), (LAtoms, NLAImps, Ant)) :-
  insert( LAImps, X, B, NLAImps). 
add_imp( Imp, (RAtoms, RImps, Succ ), (RAtoms, [Imp | RImps], Succ ) ). 

% tests
on_atom( X, (Atoms, _, _) ) :- on(X, Atoms), !.  
  % true iff X is an atom that has been processed on this side.
reduced( (_, _, []) ).
  % a side of a sequent is 'reduced' iff the unprocessed part is empty

% destructors
get_atom_imps((LAtoms, LAImps, Ant), X, B, (LAtoms, RestAImps, Ant)) :-
  extract(LAImps, X, B, RestAImps).
get_imps( ( _, Imps, _) , Imps).
get( (Atoms, Imps, [ A | Rest]), A,  (Atoms, Imps, Rest) ).


%------------------------------------------------------------------
% Dealing with lists of atomic implications


% AtomImps is an ordered list PL of pairs (X,B) where B is a formula
% and pv(X) is an atom
% lists PL are ordered by @< relation on first conponent
% B is conjunction of formulae.

% meaning( []) = true
% meaning( ( Pair | Rest|) = meaning( Pair) & meaning(Rest)
% meaning( (X,B) ) = pv(X) -> B

% extract( AtomImps, X,  B, RestImps)
% called with AtomImps and X known; returns B and RestImps
% thus  meaning(AtomImps) ==  meaning(pv(X)->B) & meaning(RestImps)

extract( [ ], _, true, []).
extract( [  Pair | AtomImps], X, B, [ Pair | RestImps ] ) :- 
  Pair = (X1, _), 
  X @> X1,                                    % still worth looking
  extract(AtomImps, X, B, RestImps). 
extract( [ (X, B) | RestImps], X, B, RestImps).      % Found it
extract( AtomImps, X, true, AtomImps) :-
  AtomImps = [ (X1, _) | _ ],  
  X @< X1.                                    % gone too far
                                   % Not there, return 'true'

% insert( AtomImps, X, B, AtomImps1)
% where pv(X) is an atom

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