Re: rule proto-proposal

From: pat hayes (
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...

It may not need to be. I just threw everything in that I thought 
might be useful. My basic rule of thumb was, if its semantic 
specification didnt involve a conditional, toss it in.

> > 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 meant the <R S T> case to be used for properties, sorry I didnt 
make that clear. I am thinking of classes as unary predicates and 
properties as binary relations.

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

I assume that we will somehow reconcile the rule-atom syntax to the 
class-inheritance syntax, but I didnt want to get involved in 
syntactic details at this stage. One wants to be able to do syntactic 
matching between the antecedents/consequents of rules and other DAML 
facts, I presume (?)

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

True, but DAML makes these distinction now, so I was respecting them.

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

I agree, it is sugar. Again, I was just trying to keep the rule-atom 
syntax in conformity to the DAML syntax. BTW, there might be a 
unification problem with having variables bound to lists. There 
certainly would be if they could have bags as values.

(BTW, whence somes this ont: prefix? Have I missed something?)

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

Well, let us put aside any potential disagreements about whether or 
not these must be URIs: the key point is that whatever they are in 
DAML, they should be the same thing in DAML-rules.
I agree there is no need to distinguish these in the syntax, by the 
way. I guess I was thinking of the relationship of the vocabulary 
used in the rules to that used in the class descriptions as being a 
bit like that between code and declarations, so that if the DAML 
statements in an ontology say that R is a property, then the rule had 
better use R in the appropriate way in order to apply to that 
ontology. (Does that make sense?) We should be able to use variables 
anywhere in the rule, of course.

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

Yes.  I thought it might be best to avoid using skolem functions in 
the rules, since in order to match with DAML class assertions, those 
would have to be able to contain functions as well, which seems like 
a big change to DAML as we currently have it.

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

After all the discussion about concrete versus abstract types and so 
on, it seemed best to avoid a situation where some rules could have 
conclusions which would constrain a datatype value. That would 
produce the kind of linkage between domain reasoning and datatype 
evaluation that the distinction was designed to avoid. It may be 
however that Peter or Ian can see some way that this relatively crude 
way of keeping them apart is inadequate. Like I say, it is a straw 

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

Ah yes. Sorry about that, I must have been partly asleep.


IHMC					(850)434 8903   home
40 South Alcaniz St.			(850)202 4416   office
Pensacola,  FL 32501			(850)202 4440   fax

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