RE: Datalog With Only Binary Relations Is Too Weak

> >     {{:gregorian :grandparent :bret} log:implies
> >      {{:gregorian :skolemfun :bret} :parent :bret}} log:implies
> >    {{:gregorian :skolemfun :bret} a :isLoved}.
>
> This is intriguing stuff...
>
> (...meaning I'm not sure that I understand the details ;^)

Well, I was hoping this was kind of selfexplanatory ...
I agree that more is needed for a proof language, this is
just something to start with ... any suggestions?

> > I try to find evidence that having (nested) dyadic formulae
> > is a good thing to limit to ...
>
> Are you referring here to the idea that the form "{:gregorian :skolemfun
> :bret}" for Skolem functions limits us to Dyadic Skolem functions?

Actually *nested* ones, such as {{{a b {c d e}} f g} h i}
or one could use DAML lists, or parameter properties which I learned from
TimBL
   ...
   and the other is in practice if you are designing by hand to create specific
   parameter properties

   endorser(e,x)
   endorses(e,y)
   withGrade(e,z)

   in N3:

   [ :endorser  :x; :endorses :y; :withGrade :z .]

   where the fact that e is an endorsement follows the some domain of the
   parameter properties.
   You can specify the type of e explicitly but you don't have to. This is a
   bit like doing both.

   [ a :endorsement;  :endorser  :x; :endorses :y; :withGrade :z .]

[this was some while ago when I was really stuck at n-ary predicates ...]
I find the *nested contexts* idea very interesting ...

--
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/

ps Graham, that ;^) looks intruiging to me ... what does it mean?