% G4IP in Prolog

:- op(840, xfy, =>).   % implies, right assoc
:- op(830, xfy, \/).   % or, right assoc
:- op(820, xfy, /\).   % and, right assoc
:- op(800,  fy, ?).    % atom, prefix

% Top-level predicates.

prove(A) :-
  seqR([], [], A).

refute(A) :-
  \+ seqR([], [], A). % negation as failure

% Auxiliary predicates.

append_([], Ys, Ys).
append_([X|Xs], Ys, [X|Zs]) :-
  append_(Xs, Ys, Zs).

memberchk_(X, [X|_]) :- !.
memberchk_(X, [_|Ys]) :- memberchk_(X, Ys).

% Implementation.

% break down asynchronous propositions first -- right then left
%   G = context of synchronous props
%   O = context of props not yet processed
% choose synchronous propositions -- right then left
%   G = context of synchronous props not yet processed
%   H = context of unused synchronous propositions

% breaking asynchronous things down on the right
seqR(O, G, A /\ B) :-
  seqR(O, G, A),
  seqR(O, G, B).
seqR(O, G, A => B) :-
  seqR([A | O], G, B).
seqR(_, _, tt).

% synchronous prop encountered on the right -- switching to the left
seqR(O, G, A \/ B) :-
  seqL(O, G, A \/ B).
seqR(O, G, ff) :-
  seqL(O, G, ff).
seqR(O, G, ?A) :-
  seqL(O, G, ?A).

% breaking asynchronous things down on the left
seqL([A /\ B | O], G, C) :-
  seqL([A,B | O], G, C).
seqL([A \/ B | O], G, C) :-
  seqL([A | O], G, C),
  seqL([B | O], G, C).
seqL([tt | O], G, C) :-
  seqL(O, G, C).
seqL([ff | _], _, _).
seqL([(D /\ E) => F | O], G, C) :-
  seqL([D => (E => F) | O], G, C).
seqL([tt => F | O], G, C) :-
  seqL([F | O], G, C).
seqL([ff => _ | O], G, C) :-
  seqL(O, G, C).
seqL([(D \/ E)=>F | O], G, C) :-
  seqL([D=>F, E=>F | O], G, C).

% synchronous left encountered -- move to gamma context
seqL([(?A) => D | O], G, C) :-
  seqL(O, [(?A) => D | G], C).
seqL([(D => E) => F | O], G, C) :-
  seqL(O, [(D => E) => F | G], C).
seqL([?A | O], G, C) :-
  seqL(O, [?A | G], C).

% context has been processed -- choose a synchronous rule
seqL([], G, C) :- chooseR(G, C).
seqL([], G, C) :- chooseL(G, [], C).

% break down synchronous prop on the right
chooseR(G, A \/ B) :- seqR([], G, A).
chooseR(G, A \/ B) :- seqR([], G, B).
chooseR(G, ?P) :- memberchk_(?P, G).
% chooseR(G, ff) :- fail. % to force a goal to fail, don't include a rule.

% break down synchronous prop on the left
chooseL([?P | G], H, C) :-
  chooseL(G, [?P | H], C).
chooseL([(?P) => B | G], H, C) :-
  append_(G, H, I),
  memberchk_(?P, I),
  !,
  seqL([B], I, C).
chooseL([(?P) => B | G], H, C) :-
  chooseL(G, [(?P) => B | H], C).
chooseL([(D => E) => B | G], H, C) :-
  append_(G, H, I),
  seqR([E => B, D], I, E),
  seqL([B], I, C).
chooseL([(D => E) => B | G], H, C) :-
  chooseL(G, [(D => E) => B | H], C).
% chooseL([], H, C) :- fail.

% Tests.

% prove( ?a => ?a ).
% prove( ?a => (?b => ?a) ).
% prove( (?a => ?b) => (?a => (?b => ?c)) => (?a => ?c) ).
% prove( ?a /\ ?b => ?b /\ ?a ).
% prove( ?a \/ ?b => ?b \/ ?a ).
% prove( (?a \/ ?c) /\ (?b => ?c) => (?a => ?b) => ?c ).
% refute( (?a => ?b \/ ?c) => (?a => ?b) \/ (?a => ?c) ).
% prove( ((?a => ?b) \/ (?a => ?c)) => (?a => ?b \/ ?c) ).
% refute( ((?a => ?b) => ?c) => ((?a \/ ?b) /\ (?b => ?c)) ).
% prove( ((?a \/ ?b) /\ (?b => ?c)) => ((?a => ?b) => ?c) ).
% prove( (?a => ?b) => (?b => ?c) => (?c => ?d) => (?a => ?d) ).
% prove( (?a => ?b) => (?a => ?c) => ?a => ?b ).
% prove( (?a => ?b) => (?a => ?c) => ?a => ?c ).
% prove( ?a => (?a => ?b) => (?a => ?c) => ?b ).
% prove( ?a => (?a => ?b) => (?a => ?c) => ?c ).
% prove( (?a => ?b => ?c) => ?a => ?b => ?c ).
% prove( (?a => ?b => ?c) => ?b => ?a => ?c ).
% prove( ?a => ?b => (?a => ?b => ?c) => ?c ).
% prove( ?b => ?a => (?a => ?b => ?c) => ?c ).
% prove( (?a => ?b) => ?a => ?b ).
% prove( ((?a => ?b) => ?c) => ((?a => ?b) => ?c) ).
% prove( (((?a => ?b) => ?c) => ?d) => (((?a => ?b) => ?c) => ?d) ).
% prove( ((((?a => ?b) => ?c) => ?d) => ?e)
%                        => (((?a => ?b) => ?c) => ?d) => ?e ).
% prove( (((((?a => ?b) => ?c) => ?d) => ?e) => ?f)
%                        => ((((?a => ?b) => ?c) => ?d) => ?e) => ?f ).
% prove( (((((?a => ?b) => ?c) => ?d) => ?e) => ?f)
%                       => (((((?a => ?b) => ?c) => ?d) => ?e) => ?f)
%                       \/ (((((?a => ?b) => ?c) => ?d) => ?e) => ?f) ).
% prove( ((?a => ?b) => ?c) => ?d => ?d \/ ?d ).