@prefix dc: <http://purl.org/dc/elements/1.1/>.
@prefix u: <http://www.w3.org/2000/01/rdf-schema#>.
@prefix : <relalg#>.

<> dc:source [ dc:description "relalg.py from gadfly" ],
 <http://lists.w3.org/Archives/Public/www-rdf-logic/2001May/0001.html>
 <http://www.acm.org/classics/nov95/toc.html>.

<http://www.acm.org/classics/nov95/toc.html>
  dc:title "A Relational Model of Data for Large Shared Data Banks";
  dc:creator "E. F. Codd";
  :reprintedFrom
   [ dc:title "Communications of the ACM";
     :vol "13"; :no "6"; dc:date "June 1970";
     :pp "377-387";
     :copyright "1970, Association for Computing Machinery, Inc."
   ].


:reprintedFrom u:subPropertyOf dc:relation; u:label "Reprinted from".
:vol u:label "Vol.".
:no u:label "No.".
:pp u:label "pp.".
:copyright u:subPropertyOf dc:rights; u:label "Copyright (c)".

@prefix dpo: <http://www.daml.org/2001/03/daml+oil#>.

:relationOver
  u:range [ :listOf u:Class ];
  a dpo:UnambiguousProperty; # theorem? prove it?
  u:comment "e.g. ex:Complex :relationOver (ex:Real ex:Real);
except that these relations are finite.".

# the empty list(tuple) is the only element of the relation over ().
[ :relationOver () ] dpo:oneOf (()).

{ { :t a [ :relationOver [ dpo:first :C1 dpo:rest :Cn] ] }
  l:means { [ is dpo:first of :t ] a :C1.
	    [ is dpo:rest  of :t ] a [ :relationOver :Cn]. }
} a l:Truth; l:forAll :t, :C1, :Cn;

:Table a u:Class;
  u:label "Table";
  :fields ( :fields :domains );
  :domains ( [ :listOf r:Property ] [ :listOf u:Class ] ).

  u:subClassOf
   [ dpo:onProperty :labels;
     dpo:toClass [ :listOf r:Property ],
   [ dpo:onProperty :domains;
     dpo:toClass [ :listOf u:Class ].


{ { :lc :listOf :C }
  l:means
    { { { :x dl:member :lc. } l:implies { :x a :C } } l:Truth; l:forAll :x }
} a l:Truth; l:forAll :lc, :C.