- From: pat hayes <phayes@ai.uwf.edu>
- Date: Mon, 19 Mar 2001 09:53:39 -0600
- To: jos.deroo.jd@belgium.agfa.com
- 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 ...
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?
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)
>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.
> > > 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.
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 10:51:56 UTC