From: Dan Connolly (connolly@w3.org)
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 http://www.w3.org/People/Connolly/
This archive was generated by hypermail 2.1.4 : 04/02/02 EST