Peter, Sandro --

I'm following your discussions (below) with great interest.

Perhaps the following is simplistic, but please point out to me where it falls short of what is needed for reasoning for the Semantic Web:

1.  For reasoning, use RDF triples notation, but restrict it to ground facts (no variables).  For storage and transport across the web use any convenient RDF notation, provided it converts easily in- and out- of triples.  (See below for reasons why ground facts are enough.)

2.  Use datalog-plus-optional-NAF rules to reason about the ground facts.  If NAF is allowed, restrict it to be stratified (no loops through negation) as in [1].

3.   Use the Apt-Blair-Walker [1] model+fixpoint theory to assign a unique semantics to a collection of ground triples+rules.  This semantics has been around for more than a decade, and as far as I know, no one has suggested that it yields results that violate our intuitions about what ought to follow from a collection of facts and rules.

4.   Use the Apt-Blair-Walker [1] interpreter as a proof theory.  For efficient practical inferencing, use  Backchain-Iteration [2], which is proven terminating, sound and complete wrt to the model+fixpoint theory in [1].

5.  Realize that it is straightforward to include type-inference and and second order reasoning in the framework outlined in points 1-4 above.  There's an example appended below, and there are further running examples at www.reengineeringllc.com .[3]

The only disadvantage of the above approach I can think of at the moment, is that type inference will have to be stated in the rules, rather than built into an execution mechanism.  But that may actually be a good thing, because it brings out into the daylight some gotchas such as  "Clyde is an elephant, and an elephant is a species, therefore Clyde is a species" .  Those kinds of errors can easily be avoided when writing rules, but may pass unnoticed if type inference is done under the covers by the execution mechanism.  Unnoticed, that is, until something disastrous happens in the real world as a result!


References:

[1] K. Apt and H. Blair and A. Walker.  Towards a Theory of Declarative Knowledge, In: Foundations of Deductive Databases and Logic Programming, J. Minker (Ed.), Morgan Kaufman 1988.

[2] A. Walker.  Backchain Iteration: Towards a Practical Inference Method that is Simple Enough to be Proved Terminating, Sound and Complete. Journal of Automated Reasoning, 11:1-22, 1993.

[3] Running examples in the Internet Business Logic system, online at www.reengineeringllc.com :  NonSubsume1,  RDFreasoning1,  ClydeElephant1,  SemanticWebOntology1,  etc.
(Some of these examples use facts whose arity is other than 3, but those can be encoded into triples in the usual way, and decoded using rules)

Example:


1)  Table heading:

    this-relationship is a specialization of this-higher-relationship
    =================================================================

This is an "X IS-A relation Y" before inserting any tuples.


2) Populate the table

    this-relationship is a specialization of this-higher-relationship
    =================================================================
    sibling                                family
    marriage                               family
    family                                 the class of all relationships


3)   Say that IS-A is transitive

    some-relationship1 is a specialization of some-relationship2
    that-relationship2 is a specialization of some-relationship3
    ------------------------------------------------------------
    that-relationship1 is a specialization of that-relationship3


4)  Say that if two people are related by R1, and R1 IS-A R2, then they are related by R2

    some-person is related through some-relationship to some-other-person
    that-relationship is a specialization of some-higher-relationship
    ---------------------------------------------------------------------------
    that-person is related through that-higher-relationship to that-other-person

 
5)   Provide some facts

    this-person is related through this-relationship to this-other-person
    =====================================================================
    Fred                           marriage              Jane
    Fred                           sibling               John


6)   Ask who is related to whom and by what relationship, and get the answer table

    this-person is related through this-relationship to this-other-person
    =====================================================================
    Fred                           family               Jane
    Fred                           family               John
    Fred                           marriage             Jane
    Fred                           sibling              John
    Fred             the class of all relationships     Jane
    Fred             the class of all relationships     John

7)  Ask for an explanation of the last line of the answer, and get this:

    Fred is related through sibling to John
    sibling is a specialization of  the class of all relationships
    ---------------------------------------------------------------- 
    Fred is related through  the class of all relationships  to John


    sibling is a specialization of family
    family is a specialization of  the class of all relationships
    --------------------------------------------------------------
    sibling is a specialization of  the class of all relationships 

The alert reader will have noted that the example has sneaked in some second-order reasoning, while staying inside datalog.

                        Thanks in advance for your comments  -- Adrian

---------------------------------------------------------------------------------------------------------------------------------

                                           INTERNET BUSINESS LOGIC
 
                                             www.reengineeringllc.com
             
Dr. Adrian Walker
Reengineering LLC
PO Box 1412
Bristol
CT 06011-1412 USA

Phone: USA 860 583 9677
Cell:    USA  860 830 2085
Fax:    USA  860 314 1029n enter the text in that file's own buffer.




At 11:43 AM 11/26/03 -0500, you wrote:

From: Sandro Hawke <sandro@w3.org>
Subject: Re: plain rules, please [was: Semantic Web Rule Language (SWRL) 0.5 released]
Date: Wed, 26 Nov 2003 10:59:57 -0500

[...]

> > Compatible in what sense? I mean, "well, the orthogonal language needed
> > to be entirely disjoint with OWL, and heck, it's also disjoint with OWL
> > rules!" or "Once we figure out how to be usefully orthogonal and yet
> > combinable with OWL, we'll find that we've subsumed OWL rules or at
> > least fit in nicely with them"?
>
> In the latter sense.
>
> > Personally, I don't yet have even a vague sense of this :(
>
> I have a strong sense of it, but as I'm sometimes reminded, that
> doesn't mean I'm right.  I think of RDF-based logics (RDFS, OWL, SWRL,
> ...) in terms of FOL axioms on sentences like "rdf(s,p,o)".  I think
> this approach is suggested by LBase, and it's what Surnia (my quick
> hack OWL implementation) does.  From this angle, orthogonality and
> combinations of logics are fairly straightforward.

OK, let's see how easy it is to break this very strong claim!

>     -- sandro

Lets think of two extremely simple RDF-like logics, which I'll call RDF0
and RDC0, and give them ``meaning'' using the mechanism above.  Both RDF0
and RDC0 are written in triples, just like RDF and RDFS, where a triple
looks like <s,p,o> where s, p, and o are all URI references (which I will
write as QNames).  The proof theories for both RDF0 and RDC0 are given by
means the above translation (T) into plain FOL plus an axiomatization
(RDF0A/RDC0A), so that
        O1 |- O2  in RDF0
iff
        T(O1),RDF0Z |= T(O2)
and similarly for RDFC0.

RDF0 has one interpreted constant, rdf0:type, whose intended meaning is the
type relationship from RDF.  The obvious, uncontroversial axiomatization of
RDF0 is the empty set of axioms - there are just no extra axioms needed at
all for this very simple logic.

RDC0 has one interpreted constant, rdc0:subClassOf, whose intended meaning
is the subclass relationship from RDFS.  The axiomatization of RDC0 is
        Ax rdf(x,rdc0:subClassOf,x)
        Ax,y,z  rdf(x,rdc0:subClassOf,y) & rdf(y,rdc0:subClassOf,z)
                -> rdf(x,rdc0:subClassOf,z)
This could be a bit controversial but note that RDC0 has no way of stating
that a URI reference denotes a class or not, so this makes the assumption
that everything is a class.  This does not really get us into trouble, and
certainly does not get us into trouble in RDC0. 

Now Sandros claim is that the combination of RDF0 and RDC0 is
straightforward.  I claim that it is not.  Certainly it is not the case
that the proof theory that results from the combination of the proof
theories of RDF0 and RDC0 gets what one wants, because
        <ex:a,rdf0:type,ex:c>,<ex:c,rdc0:subClassOf,ex:d>
does not imply
        <ex:a,rdf0:type,ex:d>
in this proof theory.

Instead a new proof theory has to be constructed for the combination of
RDF0 and RDC0.  This new proof theory may be a superset of the union of the
proof theories the two component logics, but it need not be.  To show this,
consider an extension of RDF0 (RDF1) that adds rdf1:Class, whose intended
meaning is as in RDFS, i.e., the class of all classes.  Now the combination
of RDF1 and RDC0 has the ability to state that something is a class, which
means that the first axiom for RDC0 should be replaced by
        Ax rdf(x,rdf0:type,rdf1:Class) -> rdf(x,rdc0:subClassOf,x)
        
So my claim is that axiomatizing logics, even using similar encodings for
both logics, does not provide a route to straightforward combination of
logics.

Peter F. Patel-Schneider
Bell Labs Research

PS:  Why then does the RDF/RDFS combination appear to work?  Well, it works
because RDFS is an extension of RDF, and thus all the hard work has been
already done in RDFS.