Usually, when similarity is not a coincidence, there is often some common abstraction that is worth factoring out.
Let’s say that I have four collections (A, B, C, and D) and four specs of those collections (W, X, Y, and Z) such that collection A has W, X, Y, and Z as its specs, just as collection C has W, X, Y, and Z as its specs. To Cyc, it’s just an interesting coincidence that they all have the same specs. But often there is a reason that the specs are all the same; there’s some common property in the middle that explains the similarity. Maybe, if the specs are all this one type of thing (P), then this one type of thing is expected of all those collections.
These sorts of N by M lattices, depicted on the left side of the slide, can be reduced to N + M statements with a judicious extraction of why it is that they all have this in common, as depicted on the right side of the slide. Reducing the number of genls or genlMt relations that have to be stated explicitly saves the system a lot of work, especially when doing inference. In fact, for any situation where you have (in the case of microtheories) more than two microtheories with more than two specsMts, (N and M are greater than 2), the savings to the system equals [(N*M) - (N+M) - (the overhead of creating one new microtheory)]. In the simple case on the slide, this comes to 8 fewer genlMt assertions. The overhead involved in using one extra microtheory is negligible.
Let’s look first at an example involving collections. Suppose that we have the following four collections (shown at the bottom of the slide): Olympic Men’s Individual 400 Meter Butterfly, Olympic Women’s Individual 100 Meter Backstroke, etc. Each collection refers to all instances of that type of event.
In order for these collections to make sense, they need to inherit from (at least) the collections above them on the slide: Olympic Competition, Individual Competition, and Swimming Competition. Thus the collections along the bottom of the slide must be made specs of the collections at the top of the slide.
So we need to create genl links from each of the more specific collections along the bottom of the slide up to the more general collections along the top of the slide. Now we have 12 (3 * 4) genl links which allow each of the lower collections to inherit from the necessary collections above.
You and I can look at this and imagine that there are probably many more possible collections of the type “Olympic <Gender> Individual <Distance> <Stroke>.” The number of genl links necessary gets very high very quickly. We can also see that there is an obvious pattern in these more specific collections. Cyc doesn’t see the pattern (coincidences are possible and we don’t want Cyc to think there is a pattern when one is not really there). Why not factor out those properties that are in common among all of these collections and tell Cyc about it?
Factor out what is in common and put it in a new collection, called Olympic Individual Swimming. Now we need only 7 (3 + 4) genls links. The four lower collections inherit from the new collection and the new collection inherits from the three upper collections. The lower collections can still see the information they need, but now it’s all collected together in one place.
The same idea works with microtheories and genlMt links. Suppose that we’re representing in the KB the contents of each day’s Sports Section from USA Today. Each #$PropositionalInformationThing (“PIT”) is its own microtheory, so we have Mts (shown at the bottom of the screen) such as: “April 15, 2002 USA Today Sports Section Mt,” “June 2, 2002 USA Today Sports Section Mt,” and so on. Each of these microtheories contain the semantic content of the sports section of USA Today from a particular day. We’ll have about 260 of these for each year that we represent (weekdays only!). So if a record-breaking event takes place on April 14th, the April 15 Mt will contain a description of that event.
In order for these Mts to make sense, they need to inherit from (at least) the microtheories above them on the slide: Rules for Games Mt (which describes how each sport is played), American Sports Competition Mt (which has information on schedules, team rosters, and which teams play in which leagues), and Current and Historical Stats Mt (has current and historical statistics). Thus the microtheories along the bottom of the slide must be made specMts of the microtheories at the top of the slide.
So we need genlMt links from each of the more specific microtheories along the bottom of the slide up to the more general microtheories along the top of the slide. Now we have 780 (3 * 260) genlMt links per year of Sports Sections, which allow each of the lower microtheories to inherit from the necessary microtheories above.
In reality, the number of genlMt links necessary would probably be greater than 3 * 260 per year because each new issue would likely have to be linked to more than 3 microtheories. We can also see that each new PIT will have to inherit from the same microtheories. So we want the PIT’s to be able to refer to all of the microtheories at the top of the slide using a single referent. We can do this by introducing one new microtheory in the middle.
Now we need only 263 (3 + 260) genlMt links to represent a year’s worth of Sports Sections. The lower microtheories inherit from the new microtheory and the new microtheory inherits from the three upper microtheories. The lower microtheories can still see the information they need, but now it’s all visible via a single Mt, the Rules, Competition, and Stats Mt.
You’ve seen how factoring out commonality saves work in inference by reducing the number of genl/genlMt links involved. Now let’s look at another one of the benefits of factoring out commonality.
First, consider how a forward rule behaves when two or more of its literals and/or the rule itself are in different Mts. Let’s say that the KB contains some microtheories (X, Y, Z, and T) and T contains a forward rule (PQR®S). The highest (most general) specMt that can see P, Q, R, and the rule, will automatically have an S asserted in it.
However, in a situation like the one on the slide, where several microtheories are all the highest (most general) specMt, poor Cyc can successfully conclude S, but it has no choice but to conclude S in all of these microtheories. If there are three hundred of these microtheories, Cyc will conclude the same S in all three hundred microtheories.
So, you should abstract out an Mt from which all of the specMts inherit. Now Cyc can conclude S in one place, and all of the microtheories below inherit that conclusion from it. Not only are there fewer genlMt links, but S is only asserted in one place, so inference involving S or any of the specMts is much simpler.
This is a very general mechanism that I encourage you to use when you have similar things like this in your system: factor out that which explains the commonality.
The fact that we have this nice, complicated, predicate logic language doesn’t mean that all constructs that one can state in this are equally easy to reason with. In particular, things that conclude #$thereExists are a little bit more expensive than others because they are basically extending the number of concepts and the symbols in the language that the system might have to think about. In order to conclude thereExists, our system introduces a function under the covers which will denote the thing that so exists so that the system can reason with it. This process is called skolemization. If you state a lot of existence statements, you will be creating a bunch of these under the covers.
It’s also a pervasive problem that existence is stated far too specifically in many cases. Thus you see things like: Every elephant has a head. Every elephant has a head with a trunk. Every cow has a head. Etc. It is very ennobling to state that things actually exist, rather than just state constraints on things would they exist. People love to state that things actually do exist.
However, it seems like you could state a very general property like uniquePartType, that matched elephant to head, and then write one very powerful rule that says for each object there exists a unique object for each of its uniquePartTypes. And you could write one very general rule that states the existence. And then you could state constraints on those things that exist more specially. If you’re writing a rule that concludes thereExists, I would strongly encourage you to generalize that as much as possible.
The case on this slide is an example of what we consider an overuse of #$not in the system. Let’s say that someone wants to write a rule that says that birds are by default capable of flying. Then they realize “oh, but not penguins” so they stick a #$not in there. Then they get hungry and go out to lunch and forget about this. Well, what about all of the other cases like those listed on the slide? Emus? Birds with broken wings? And all of these other exceptions that would make it unable to fly?
These are exceptions and they deserve to be treated exceptionally. In our system, it does not make sense to state these rare, negated checks directly in the rule. This is mixing together the intent of the rule with meta-knowledge about when the rule doesn’t apply in the rule itself. It’s good to separate the two.
Because we support default reasoning in our system, the best thing to do in the situation described on the previous slide would be to state the nice general rule that you want (i.e. birds are by default capable of flying) and then state exceptions to it. So this rule has an exception to it where if the bird is a flightless bird, then this rule doesn’t apply. Then you can add some nice ontologizations of penguins, emus, dodo birds -- all kinds of flightless birds.
In our system, when we produce a candidate inference, and we find a rule that was used to produce it, if that rule has exceptions stated about it, then, at the very end, we can easily check to see if the exceptions are true. Since these are by default exceptional, they are rarely true; so we save a lot of work by postponing this check until the end when we have to. So when you see yourself writing #$not’s in the antecedent, you should ask yourself “is this really part of the warrant of the rule? Is this what the rule really means or this a meta-statement about cases where that rule wouldn't apply and should be stated as an exception?” If it’s the latter, then use exceptions.
Other systems, that use negation by failure as a primary negation mechanism, sort of assume that you have all of this stuff that’s stated that is true and by default if it isn’t stated in the system then assume it’s not true. That’s how they get some of their “not”s. This case is an example of underuse of #$not. It’s much better to be able to strongly conclude that something is not true than to assume it’s not true. This is especially the case in our system, because we often use negations to prove inferences. Negations are the very thing that allow you to do most of the interesting pruning.
We have some very powerful vocabulary to state negations in our system. #$disjointWith between two collections allows you to state that none of the things in this collection are going to be in that collection. #$disjointWith between #$partiallyTangible and #$intangible implies trivially on the order of ten billion negations -- one single #$disjointWith plus the reasoning involved. Do I have to assume that a table is not an integer? No. I don’t have to assume that because one #$disjointWith covers that and billions of other reasons that things aren’t other things.
A very powerful form of #$disjointWith is to state that each thing in an entire taxonomy of collections have this interesting property. This is what #$SiblingDisjointCollection is for. Like the Linnean taxonomy of life which says that for everything, either one is a spec of the other, or they’re disjoint. This gives you a nice perfect tree. Saying #$ SiblingDisjointCollection about animal taxonomic type allows you to conclude that a chicken is not a giraffe, a giraffe is not a wildebeest, a wildebeest is not a wombat, etc. All of these things from one statement and knowledge about the Linnean taxonomy.
Two other interesting predicates are #$completeExtentKnown and #$completeCollectionExtent. The former applied to a predicate says “the complete extent of this predicate is stated in the KB. So if it’s not there it’s false.” This is useful for things like #$nationalBorder. There are only so many countries in the world and they all have on average something like 2 or 3 borders, right? So with about 700 or fewer assertions you could state every border in the world and then state that’s it, that’s all of them. Then you could reason that Canada does not border on France just from knowing that I don’t know it and I know I should know it if it’s there.
The analog for collections is #$completeCollectionExtent. I strongly encourage you to use this predicate about certain collections that are complete. This allows you to iterate over the current instances of the collection in inference rather than always having to wait until some other part of inference returns candidate instances. A good example of this is #$MonthOfYearType (this is based on the Julian Calendar with January, February, March, etc,.). There are only twelve of those -- there is not going to be a thirteenth. So once you have all twelve stated, tell the system that that’s it.
Note that these talk about the current theory only. So as far as the current theory is concerned, those are all of the months. In the future, if the world changed and we were to add “Yule” as something between December and January, a new two-day month, then we could update that and then there would be thirteen months and that would be all of them. Go ahead and use these things; and in the future, if you add something new, it just means that the theory has been revised, just like any other -- just like adding any other new vocabulary.
The example on the slide is a particular overuse of #$or which I call “list-em” KR. People just start listing stuff in an order that hints at what they’re trying to get at. Consider the rule on the slide about sibling rivalry. It says “if there’s a person and there’s something which is either that person’s brother or their sister, then they feel rivalry towards them. Remember #$or can be an arbitrary disjunction. So following the #$or you could have something which is their sister or their hair is green or something else. This rule on the slide is a case where the intended meaning of #$or is not arbitrary. There’s an intended commonality among these two things. They are skipping around this concept of sibling. What they really should have is a predicate called #$siblings. If there was this predicate called #$siblings, which had #$brothers and #$sisters as specPred’s, then this would would be a very simple rule.
If you’re writing sentences that have #$or’s in them, ask yourself if there is some generalization that you’re wishing was there, that you’re having to describe and circumscribe around with your disjunction instead of a more appropriate predicate. Rules like the one on the slide devolve into proof by cases. Proof by cases, however, can be handled much more efficiently using genlPred’s if they already exist.
This is very Cyc-specific. We have a version of not equals called #$different. #$different can take any number of items and state that they all have to be different. So if you have n number of items, rather than writing n2/2 not equals statements, you can just say that they’re all different and this has a nice HL module for implementing it that has a fail fast if two things that are similar show up in it. This is good for pruning, too.
- Factor out Commonality
- Existence is Expensive
- Exceptions are Exceptional
- State Negations Explicitly
- Generalize - Don’t List
- Use #$different
- Avoid (#$not (#$equals ...))
This concludes Part 2 of the lesson called “Writing Efficient CycL.”