#negation-as-failure

Forward chaining with rule-ordering conflict resolution (each step fires the first rule, in list order, that can add something new):

P0: IF ?x has sharp teeth                              THEN ?x is a carnivore
P1: IF ?x has three horns                              THEN ?x is a Triceratops
P2: IF ?x is a carnivore AND ?x has big arms           THEN ?x is a Deinonychus
P3: IF ?x is a carnivore AND ?x hunts ?y               THEN ?x is a TRex
P4: IF ?x has sharp teeth AND NOT(?x is a Deinonychus)
       AND ?y is a Triceratops                         THEN ?x hunts ?y

Assertions: Spike has three horns; Fido has sharp teeth; Fido has big arms;
            Rover has sharp teeth; Spike has flat teeth

NOT matches only if no matching assertion is present at that moment. With this order the run ends with Fido a Deinonychus and Rover a TRex that hunts Spike. What changes if P4 is moved to the front of the list?