%
%  RDF Negation defined with a class (lx_FalseSentence) and
%  three predicates (lx_subject, lx_predicate, lx_object).
%
%  We turn self-reference paradoxes into contradictions by 
%  declarating that these sentences are stratified; that is
%  sentences are always "higher" than their parts.
%
%  Alas, I cannot prove these axioms are consistent!
%
%  The general problem I'm working on is discussed in 
%  http://lists.w3.org/Archives/Public/www-rdf-logic/2002Sep/0013.html
%

%  Some stuff to help keep otter complete & happy
set(auto).
clear(control_memory).
assign(max_seconds, 31000000).
assign(max_mem, 500000).
set(prolog_style_variables).

formula_list(usable).

%
%   Connect -rdf with its reification
%

all X Y Z (
  (exists S (
    rdf(S, rdf_type, lx_FalseSentence) &
    rdf(S, lx_subject, X) &
    rdf(S, lx_predicate, Y) &
    rdf(S, lx_object, Z)
  ))
  <->
  -rdf(X, Y, Z)
).

%
%   Stratify sentences (anything which describes
%   a looping sentence is false).
%

%% A sentence is higher than its parts

all S P (
  rdf(S, lx_subject, P) 
  ->  
  higher(S, P)
).

all S P (
  rdf(S, lx_predicate, P) 
  ->  
  higher(S, P)
).

all S P (
  rdf(S, lx_object, P) 
  ->  
  higher(S, P)
).

%% "higher" is antisymmtric (like greater-than)

all S1 S2 (
  higher(S1, S2) -> -higher(S2, S1)
).

%% "higher" is transitive (like greater-than)

all S1 S2 S3 (
  higher(S1, S2) &
  higher(S2, S3) 
  -> 
  higher(S1, S3)
).


%
% There might be a kind of empty or singleton universe where this would be
% consistent.  Am I interested in that kind?
%

rdf(c1,c1,c1).
-rdf(c2,c2,c2).

%%   %
%%   % Example 1
%%   %
%%   
%%   % indirectly assert -rdf(a,b,c)
%%   rdf(s, lx_subject, a).
%%   rdf(s, lx_predicate, b).
%%   rdf(s, lx_object, c).
%%   rdf(s, rdf_type, lx_FalseSentence).
%%   
%%   % directly assert(a,b,c)
%%   rdf(a,b,c).
%%   
%%   ---------------- PROOF ----------------
%%   
%%   1 [] -rdf(A,rdf_type,lx_FalseSentence)| -rdf(A,lx_subject,B)| 
%%        -rdf(A,lx_predicate,C)| -rdf(A,lx_object,D)| -rdf(B,C,D).
%%   16 [] rdf(s,lx_subject,a).
%%   17 [] rdf(s,lx_predicate,b).
%%   18 [] rdf(s,lx_object,c).
%%   19 [] rdf(s,rdf_type,lx_FalseSentence).
%%   20 [] rdf(a,b,c).
%%   777 [hyper,20,1,19,16,17,18] $F.
%%