Tell Cassie the following information (note, by the way, that we are ignoring tense): |
(describe (assert member Marcus class man))
(describe (assert member Marcus class Pompeian))
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) |
(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.
(describe (assert member Caesar class ruler))
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.
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.
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))))
(describe (assert arg1 Marcus rel try\ to\ assassinate arg2 Caesar))
(describe (deduce arg1 Marcus rel loyal\ to arg2 Caesar))
(describe (add forall *m ant (build member *m class man) cq (build member *m class person)))