% This Prolog program has been developed with SWI Prolog and may
% contain procedures that are not standard (numbervars).
% SWI Prolog is free and can be found at: http://www.swi-prolog.org/
% To run this file, enter at the Prolog prompt: ['NLg.pro'].
% and then: test.
% The output is part of this file NLg.pro in the form of comments.

:- op(1200, xfx, =>).
:- dynamic e/2,r/2,s/2,false/0,dom/1.

% Format of the geometric theory.
% Lhs: conjunction of atoms, separated by commas.
% Rhs: disjunction of conjunctions that are each taken to be 
% existentially closed wrt the variables not occurring in the lhs; 
% these variables must be different  in different disjuncts
% in order to avoid nameclashes! Examples: 
% p(X) => q(X,Y);r(X,Y),p(Y) is wrong because of Y
% p(X) => q(X,Z);r(X,Y),p(Y) is right because of Z
% Range restriction: e.g. reflexivity becomes dom(X) => E(X,X).
% This GL checker is incomplete due to Prolog's search strategy.
% Some suggestions to be as complete as possible:
% Horn part before disjunctive part, Horn closure must be finite. 
% Disjunctive axioms leading to infinite paths last.
% Completeness can be achieved with a breadth-first search.

% geometric theory NLg

true => dom(par(0)).
true => dom(par(1)).
true => dom(par(2)).
true => s(par(0),par(1)).
true => s(par(0),par(2)).
dom(X) => e(X,X).
e(X,Y) => e(Y,X).
e(X,Y) => s(X,Y).
r(X,Y) => s(X,Y).
s(X,Y),s(Y,Z) => s(X,Z).

r(X,Y),r(X,Z) => s(Y,U),s(Z,U).
r(par(0),X),s(X,Y),s(X,Z) => s(Y,U),s(Z,U).
s(X,Y) => e(X,Y);r(X,Z),s(Z,Y). %last to avoid infinite path

goal :- s(par(1),X),s(par(2),X).

% end of theory, begin of GL checker

valid(Goal , _ , Stack) :- (false,nl,write('falid, stack:');    
                             Goal,nl,write('valid, stack:')),
                           nl,report(Stack).
valid(Goal,Parnum,Stack):- (Conj => Disj),Conj,not(Disj), %no model yet
                           !,           %commit to this geometric axiom
                           (Disj=(E;D)->         % IF length>1 THEN ...   
                           (nl,write('stack pushed:'),nl,
                            report([Disj|Stack]),
                            process(E,Goal,Parnum,[D|Stack]),
                            write(popfalse),nl,nl);         %  ELSE ...
                            insaddsub(mono,Goal,Parnum,Stack,Disj)).

process(E,G,P,[(E1;D)|S]) :- !,insaddsub(poly,G,P,[(E1;D)|S],E),
                               process(E1,G,P,[D|S]).
process(E,G,P,[E1|S])     :- insaddsub(poly,G,P,[E1|S],E),
                             insaddsub(poly,G,P,[false|S],E1).
                      
insaddsub(M,Goal,Parnum,Stack,E) :- 
                         numbervars(E,par,Parnum,Parnew), % instantiate
                         addpars(Parnum,Parnew),addconj(E),
                        (M=poly->write('stack top tailed'),nl,nl;true),
                         valid(Goal,Parnew,Stack),
                         subconj(E),subpars(Parnum,Parnew).
    
addpars(P,Q) :- P<Q -> assertz(dom(par(P))),R is P+1,addpars(R,Q);true.

subpars(P,Q) :- P<Q -> retract(dom(par(P))),R is P+1,subpars(R,Q);true.

addconj((A,C)) :- !,assertz(A),write(add(A)),write(,),addconj(C).
addconj(A)     :- assertz(A),write(add(A)),nl.

subconj((A,C)) :- !,retract(A),subconj(C).
subconj(A)     :- retract(A).

% end of checker, begin of user interface

test :- cleanup,!,valid(goal,3,[]).

cleanup :- forall(dynamic_not_built_in(X),retractall(X)).

dynamic_not_built_in(X) :- predicate_property(X,dynamic),
                           \+predicate_property(X,built_in).

 report(S)     :- freport(S);true. % freport reports and then fails
freport([])    :- write(stackbottom),nl,nl,fail. % to undo bindings
freport([D|S]) :- dpretty(D),nl,freport(S).
dpretty((E;D)) :- !,epretty(E),write(' OR '),dpretty(D).
dpretty(E)     :- epretty(E).
epretty(E)     :- numbervars(E,x,1,N),
                  (N>1-> write('EX '),
                        (N=2->write(x(1));
                              M is N-1,write(x(1-M))),write(' : ');
                         true), cpretty(E).
cpretty((B,C)) :- !,write(B),write(','),cpretty(C).
cpretty(B) :- write(B).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%output%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

 
%add(dom(par(0)))
%add(dom(par(1)))
%add(dom(par(2)))
%add(s(par(0), par(1)))
%add(s(par(0), par(2)))
%add(e(par(0), par(0)))
%add(e(par(1), par(1)))
%add(e(par(2), par(2)))
%add(s(par(0), par(0)))
%add(s(par(1), par(1)))
%add(s(par(2), par(2)))
%
%stack pushed:
%e(par(0), par(1)) OR EX x(1) : r(par(0), x(1)),s(x(1), par(1))
%stackbottom
%
%add(e(par(0), par(1)))
%stack top tailed
%
%add(e(par(1), par(0)))
%add(s(par(1), par(0)))
%add(s(par(1), par(2)))
%
%valid, stack:
%EX x(1) : r(par(0), x(1)),s(x(1), par(1))
%stackbottom
%
%add(r(par(0), par(3))),add(s(par(3), par(1)))
%stack top tailed
%
%add(e(par(3), par(3)))
%add(s(par(3), par(3)))
%add(s(par(0), par(3)))
%
%stack pushed:
%e(par(0), par(2)) OR EX x(1) : r(par(0), x(1)),s(x(1), par(2))
%false
%stackbottom
%
%add(e(par(0), par(2)))
%stack top tailed
%
%add(e(par(2), par(0)))
%add(s(par(2), par(0)))
%add(s(par(2), par(1)))
%
%valid, stack:
%EX x(1) : r(par(0), x(1)),s(x(1), par(2))
%false
%stackbottom
%
%add(r(par(0), par(4))),add(s(par(4), par(2)))
%stack top tailed
%
%add(e(par(4), par(4)))
%add(s(par(4), par(4)))
%add(s(par(0), par(4)))
%add(s(par(3), par(5))),add(s(par(4), par(5)))
%add(e(par(5), par(5)))
%add(s(par(5), par(5)))
%add(s(par(0), par(5)))
%add(s(par(1), par(6))),add(s(par(5), par(6)))
%add(e(par(6), par(6)))
%add(s(par(6), par(6)))
%add(s(par(0), par(6)))
%add(s(par(3), par(6)))
%add(s(par(4), par(6)))
%add(s(par(2), par(7))),add(s(par(5), par(7)))
%add(e(par(7), par(7)))
%add(s(par(7), par(7)))
%add(s(par(0), par(7)))
%add(s(par(4), par(7)))
%add(s(par(3), par(7)))
%add(s(par(1), par(8))),add(s(par(7), par(8)))
%add(e(par(8), par(8)))
%add(s(par(8), par(8)))
%add(s(par(0), par(8)))
%add(s(par(3), par(8)))
%add(s(par(2), par(8)))
%
%valid, stack:
%false
%false
%stackbottom
%
%popfalse
%
%popfalse