% $Id: owlAx-oneOf.otter,v 1.2 2003/08/01 04:24:32 sandro Exp $
formula_list(usable).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%   owl_oneOf
%
%        thing a Foo.  Foo owl_oneOf ( a b c ... )
%   to be in the class means to be equal to one of the list members

all CLASS LIST (
   rdf(CLASS, owl_oneOf, LIST)
   ->    % BIDIR
   (all INST (
      rdf(INST, rdf_type, CLASS) <-> inList(INST, LIST)
   ))
).

all MEMBER LIST HEAD TAIL (
   ( rdf(LIST, rdf_first, HEAD) &
     rdf(LIST, rdf_rest, TAIL) )
   ->
   ( inList(MEMBER, LIST)
     <->
      ( rdf(MEMBER, owl_sameAs, HEAD) |
        inList(MEMBER, TAIL) )
    )
).

all MEMBER (-inList(MEMBER, rdf_nil)).


% $Log: owlAx-oneOf.otter,v $
% Revision 1.2  2003/08/01 04:24:32  sandro
% intermediate; about to play with paramodulation
%