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 ...
>
> It is not self-explanatory. In fact it is completely opaque; I don't
> even know how to parse it. Does this notation have any syntactic
> rules, or any semantics?

notation is notation3, see http://www.w3.org/DesignIssues/Notation3.html

> The above appears to have the overall structure
> (A implies B) implies C
> which is rather unlikely, if 'log:implies' means logical implication,
> because that is equivalent to the conjunction
> (A or C) and (B implies C)

Of course, how could I be so stupid ...
If we assume following axioms
  A->B      i.e. A log:implies B.
  B->C
then the proof of C should look like
  A->(B->C)
and not like I've done so far!
Only then we have the tautology
  ((A->B)&(B->C))->(A->(B->C))
isn't it?

> > I agree that more is needed for a proof language, this is
> > just something to start with ... any suggestions?
>
> Well, there are rather a lot of proof languages out there, and many
> of them have powerful provers implemented already, so I wonder why
> you are going to all this trouble to re-invent an old wheel (?) For
> deductive efficiency, stick to the Horn clause subset of first-order
> logic. You could probably use some recent implementation of Prolog if
> you want to really burn rubber, for example.

Don't worry, we like/use all these (XSB, ...)
I remember (I was an engineering student): make things "as good as possible"
and that is never ending ... webizing ...

> > > > 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}
>
> Could you (or someone) explain what this means? Which of the symbols
> here are functions, and what are they being applied to? It could be
> read any number of ways as it stands.

It's just notation3 syntax with lot's of {subject verb object} things ...
(and h is the skolem functor)

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

Received on Monday, 19 March 2001 18:00:03 UTC