RE: Datalog With Only Binary Relations Is Too Weak

> [Pat]
> You talk above about a  PROOF of C from A->B and B->C, which I guess
> I don't understand since C doesnt follow from those two premises. Do
> you mean a proof of C from those two implications plus the assumption
> A?

definitely (I should also sleep more instead of giving half-baken replies;-)

> That would go
> A + A->B ==> B + B->C ==> C
> using forward reasoning. Written as resolution and using backward
> inference, it would be
>
> C->    B->C
> ------------
>     B->          A->B
>      ---------------
>           A->          ->A
>          ---------------

Are you suggesting a notation for the ------------ or the above ==> ?
Is it something like *log:entails* or what could it be (and fitting
with http://www.w3.org/DesignIssues/Notation3.html )?

> > > > 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 ...
>
> Not clear to me yet how the webizing changes the LOGIC that you need,
> at least at the propositional level. It needs new ways to talk about
> collections of facts, but inferences are the same on the web as
> everywhere else.

Of course the LOGIC was/is/will_be out there.
New ways to talk about collections of facts is indeed a very good point
in the light of *implicit things made explicit*.

> > > > > > 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 ...
>
> Unfortunately, that doesnt tell me what it *means*, only how it is
> implemented. If all the verbs are supposed to be functions, then this
> translates into the following logical term, where every function has
> two arguments:
> h( f( b(a, d(c, e)), g), i)
> Would that capture the intention? If so, I agree that an inference
> process needs to be able to generate such things. Again, modern
> Prolog unifiers can do this about as fast as the bits can be moved.

Exactly, and I more than agree with that last statement ...
[I'm actually in the process of generating a (geometrical) *circle thing*
with a mechanism I found (in 1980 I think) and (without going in full detail)
it does that by selecting bit pairs and using them to step in the X,Y plane.
These bit pairs are selected from the binary representation of the
differentials deltaX=Y and deltaY=-X in a way that the most significant
bit pair is choosen twice as much as the second most significant
bit pair and so on ... (there is also some nice limit-cycling
(typical non-linear control engineering stuff) involved here ...)
Well, this is just to say that those *bits* are moving slower
than the unifiers in our kind of Robinson resolution engine part ...]

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

Received on Tuesday, 20 March 2001 06:37:41 UTC