Inference in daml

Hi folks,

I've been working with expressing inference rules in daml and need a little help/feedback.

It seems that rules with just the subject unbound can be expressed easily.

For example the rule:
    type(X,animal)<-type(X,dog)
can be expressed as:
    type(X,animal) or not(type(X,dog))
or in daml:

<unionOf parseType="daml:collection">
    <Class>
        <Restriction>
            <onProperty rdf:resource="rdf:type"/>
            <hasValue rdf:resource="animal"/>
        </Restriction>
    </Class>
    <Class>
        <complementOf parseType="daml:collection:>
            <Class>
                <Restriction>
                    <onProperty rdf:resource="rdf:type"/>
                    <hasValue rdf:resource="dog"/>
                </Restriction>
            </Class>
        </complementOf>
    </Class>
</unionOf>
    
You can of course join a number of rules together with an intersectionOf. In the end all you have done is define a class. How would you actually assert the rules? by asserting that all things are members/instances of that class?

What about rules with the object (and subject) unbound?

For example a transitive rule of isa-ness might be defined as:
    isa(A,C)<-isa(A,B) and isa(B,C)
or
    isa(A,C) or not(isa(A,B)) or not(isa(B,C))

what is the daml equivalent? here's an attempt -- not sure if it pulls off what I'm trying to do...

<unionOf parseType="daml:collection">
    <Class>
        <Restriction>
            <onProperty rdf:resource="isa"/>
            <toClass rdf:resource="C">
        </Restriction>
    </Class>
    <Class>
        <complementOf parseType="daml:collection:>
            <Class>
                <Restriction>
                    <onProperty rdf:resource="isa"/>
                    <toClass rdf:resource="B">
                </Restriction>
            </Class>
        </complementOf>
    </Class>
    <Class>
        <complementOf parseType="daml:collection:>
            <Class rdf:ID="B">
                <Restriction>
                    <onProperty rdf:resource="isa"/>
                    <toClass rdf:resource="C">
                </Restriction>
            </Class>
        </complementOf>
    </Class>
</unionOf>

What about rules with the predicate unbound? seems like those might be a problem since the range of onProperty is an object/property  (not a class). I suppose the only types of rules you might want to define in this case would be things like transitivity -- which are dealt with in the language already.

Assuming you wanted to translate the daml "rules" back into your language of choice (i.e. just use daml for serialization/interchange of rules), additional information is necessary to preserve any information about how the rule should be applied efficiently (and with original intent). for example:
     a<- not(b) and not(c) becomes a or b or c as a daml rule.
which could be interpreted as any of the following:
    a<-not(b) and not(c) 
    b<-not(a) and not(c)
    c<-not(a) and not(b)
    a or b <- not(c)
    etc.
Since the collections are unordered, you can't really establish a convention that the first term/class defines the head of the rule/consequent. Has anyone dealt with this yet?

Thanks for any corrections/comments/feedback.

Geoff