From: pat hayes (phayes@ai.uwf.edu)
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 man. > > 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. Pat --------------------------------------------------------------------- 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
This archive was generated by hypermail 2.1.4 : 04/02/02 EST