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}.
> > > >
>.....
> > 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?

Yes, that follows, but kind of trivially, since if (B->C) then 
(A->(B->C)) no matter whether A is true or false. And the reverse:
*** ((A->B)&(B->C)) <- (A->(B->C))
is not valid.
I think the equivalence you want might be this:
((A&B)->C) <-> (A->(B->C))
which is both valid and nontrivial (?)

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? 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
         ---------------

> > > 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.

> > > > > 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.

Pat Hayes

---------------------------------------------------------------------
IHMC					(850)434 8903   home
40 South Alcaniz St.			(850)202 4416   office
Pensacola,  FL 32501			(850)202 4440   fax
phayes@ai.uwf.edu 
http://www.coginst.uwf.edu/~phayes

Received on Monday, 19 March 2001 19:58:08 UTC