- From: <jos.deroo.jd@belgium.agfa.com>
- Date: Mon, 19 Mar 2001 10:01:10 +0100
- To: GK@ninebynine.org
- Cc: www-rdf-logic@w3.org
> > {{: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?
Received on Monday, 19 March 2001 04:02:05 UTC