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:

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

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

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.