Re: rule proto-proposal

From: Dan Connolly (
Date: 05/31/01

pat hayes wrote:
> I would propose allowing rules of the form
> A1 A2.... An -> C
> where n>=0, ie Horn clauses, where the Ai and C are atoms. (Some
> atoms may only occur in antecent position, however.)
> C may be empty, ie rules of the form
> A->
> are allowed. An empty consequent is interpreted to be 'false', so
> this is in effect a negation, in the usual way.

Yes, something like that is what I'm interested in.

I'm not sure why the specification of atoms and terms
is so involved...

> An atom is an expression of one the following forms:
> <subclassOf S T>
> <subPropertyOf S T>
> <sameClassAs S T>
> <samePropertyAs S T>
> <sameIndividualAs S T>
> <disjointWith S T>
> <differentIndividualFrom S T>
> <complementOf S T>
> <unionOf S L>
> <disjointUnionOf S L>
> <intersectionOf S L>
> <oneOf S L>
> <R S T>
> <S T>
> <rdf:value S T>

Doesn't <R S T> subsume all of those, where R, S, and T
are terms, and terms are either constant symbols (URIs),
strings, or variables?

i.e. the form of the rules is orthogonal to the rest
of the DAML vocabulary, no?

> where R is a property name,

i.e. a constant symbol/URI. check.

We don't need to distinguish property/predicate symbols
from other symbols; if you want to look at these
atoms as 1st order formulas, they all have the same,
implicit, predicate symbol, ala holds in KIF
or PropertyValue in the DAML axiomatic semantics.

> S and T are terms, and L is either a
> variable or a list of terms.

I don't mind syntactic sugar for lists, but recall
that we don't need it:
	(ont:unionOf ?X (Animal Vegeteble))
reduces to
	(ont:unionOf ?X L1)
	(ont:first L1 Animal)
	(ont:rest L1 L2)
	(ont:first L2 Vegetable)
	(ont:rest L2 nil)

> A term is either a class name, a
> datatype or a variable.

Why distinguish those in the syntax?
It seems necessary and sufficient to use URI constant
symbols for all of them.

> Expressions of the form
> <rdf:value S T>
> <unionOf S L>
> <disjointUnionOf S L>
> <intersectionOf S L>
> <oneOf S L>
> and <R S T> where R is a Datatype property, and any expression
> mentioning a datatype, are allowed only in antecedents.

I can see why you don't allow list syntax in conclusions, since
they're shorthand for existential/skolem thingies.

But why the special cases for rdf:value and <R S T>?

> I would also suggest that we allow simple equality statements, at
> least in the consequents, even though these are not currently in DAML.

Huh? yes they are:

	(ont:equivalentTo ?X ?Y)

Dan Connolly, W3C

This archive was generated by hypermail 2.1.4 : 04/02/02 EST