7.2. Asserting Rules

Tell Cassie the following information (note, by the way, that we are ignoring tense):

1. Marcus was a man.

   (describe (assert member Marcus class man))

2. Marcus was a Pompeian.

   (describe (assert member Marcus class Pompeian))

3. All Pompeians were Romans.

   To assert this, we need some relations that are built into SNePS for use in node-based inference. These include:
   

   forall	which is used to represent the universal quantifier (UM§3.1.2)
   ant	which is used to represent the antecedent of an if-then rule (UM§3.1.1)
   cq	which is used to represent the consequent of the rule (UM§3.1.1)

   
   The node that SNePS builds at the head of a forall arc is a variable node, in this case representing a universally quantified variable (UM§1.5). The nodes that SNePS builds at the heads of ant and cq arcs can be pattern nodes that SNIP, the SNePS Inference Engine, uses to match other nodes in the network as part of the inference process (UM§1.5). Note in the following SNePSUL command the use of $ SNePSUL variables and the * operator.

   (describe (assert forall $p
                     ant (build member *p class Pompeian)
                     cq  (build member *p class Roman)))
   

   This says: For all p, if p is a member of the class Pompeian, then p is a member of the class Roman; i.e., for all p, if p is Pompeian, then p is Roman; i.e., all Pompeians are Romans.
4. Caesar was a ruler.

   (describe (assert member Caesar class ruler))

5. All Romans were either loyal to Caesar or hated him.

   Here, we need some more logical notation, and some more relations. First,

   define the relations:

   (define arg1 rel arg2)
   

   Next, the new notation. We need to express disjunction. Let's use exclusive disjunction. In ordinary first-order logic, exclusive disjunction is a connective that takes only 2 propositions. In SNePS's logic, there is a "connective" that is a generalization of conjunction, disjunction, and several others, which takes an arbitrary number of propositions. It is called and-or. The built-in relations used to represent it are min and max. In general, min X max Y arg (P1 ... Pn) is interpreted as: at least X and at most Y of the propositions P1, ... , Pn are true. Thus, e.g., if X = 0 and Y = 0, we have a generalized negation. If X = n and Y = n, we have a generalized conjunction. If X = 1, Y = 2, and n = 2, we have inclusive disjunction. If X = 1, Y = 1, and n = 2, we have exclusive disjunction, which is what we want for "All Romans were either loyal to Caesar or hated him." So,

   evaluate:

   (describe (assert forall $r
                     ant (build member *r class Roman)
                     cq  (build min 1 max 1
                                arg ((build arg1 *r
                                            rel loyal\ to
                                            arg2 Caesar)
                                     (build arg1 *r
                                            rel hate
                                            arg2 Caesar)))))
   

   This says: For all r, if r is Roman, then at least 1 and at most 1 of the following two propositions is the case: r is loyal to Caesar, r hates Caesar.

6. Everyone is loyal to someone.

   Here, we might say: For all m, if m is a man, then there is a y such that m is loyal to y. (Of course, not everyone is a man; we can fix this later.) This might be done with an existential quantifier arc. Instead, however, we use the technique of Skolem functions. We will have a Skolem function that takes as its argument a person and returns the individual that that person is loyal to. First,

   define a new relation:

   (define skolem-function)
   

   Next, we need a way to describe the individual to whom someone is loyal; so, call this individual the "liege of" the man who is loyal. Putting this altogether, we have:

   (describe (assert forall $m
                     ant (build member *m class man)
                     cq  (build arg1 *m
                                rel loyal\ to 
                                arg2 (build skolem-function liege\ of
                                            arg1 *m))))
   

   This says: For all m, if m is a man, then m is loyal to the liege of m.
7. People only try to assassinate rulers they are not loyal to.

   Here, we need negation, for which we'll use min 0 max 0, as described above. We'll also need to have a conjunction in the antecedent: For all ppl and all rlr, if ppl is a person, and rlr is a ruler and ppl tries to assassinate rlr, then ppl is not loyal to rlr. This is done using the built-in SNePSUL relation &ant:

   (describe (assert forall ($ppl $rlr)
                     &ant ((build member *ppl class person)
                           (build member *rlr class ruler)
                           (build arg1 *ppl 
                                  rel try\ to\ assassinate
                                  arg2 *rlr))
                     cq (build min 0 max 0
                               arg (build arg1 *ppl
                                          rel loyal\ to
                                          arg2 *rlr))))
   

8. Marcus tried to assassinate Caesar.

   (describe (assert arg1 Marcus
                     rel try\ to\ assassinate
                     arg2 Caesar))
   

9. Was Marcus loyal to Caesar?

   (describe (deduce arg1 Marcus rel loyal\ to arg2 Caesar))
   

10. Oops! We forgot to tell Cassie that all men are persons. We can use forward inference to do this. I.e., we can tell Cassie a new rule, that all men are persons, and then we can immediately have Cassie perform forward inference using this new rule. This is done with the SNePSUL command add, which is syntactically just like assert:

    (describe (add forall *m
                   ant (build member *m class man)
                   cq  (build member *m class person)))