Testing in Your Own Microtheory

In the previous two steps, we created some constants (including a new microtheory called #$Cats-PracticeMt) and we made some new assertions. In Step 4, we'll be testing Cyc to make sure that the implications of those new assertions are there. If you have not yet created those new constants and/or assertions, please go back and complete Step 2 and Step 3.

We are not finished yet, however! Just as a good engineer does not just design and build things, but also tests those things to see if they are doing what they are supposed to do, an ontologist must do the same.

Question: How does one test an ontology?

Answer: Using the Cyc inference engine!

We will now explore Cyc's question-and-answer functionality. Let's go back to the Tools page and click on "Ask".

Try it yourself! Enter this into your copy of OpenCyc.    Click on the Tools link in the left corner of the top frame.   [ Show me ] This will bring up the "Browser Tools" page. Click on the "Ask" link in the column on the left.   [ Show me ] This will bring up the "Ask a Query" page.

As an ontologist, having finished making some assertions I will ask myself, what are some things that I would expect Cyc to know based on the information I've just entered? Of course I would expect Cyc to know (isa Billy DomesticPet) and (likesAsFriend Billy Peter) as I explicitly asserted those. But what about something a little less obvious, something that will make Cyc think a bit? ...What could such a question be? What about, say, the fact that Billy takes up space?

Let's ask.

Try it yourself! Enter this into your copy of OpenCyc.    Enter "(isa Billy SpatialThing)" in the large text box.   [ Show me ] Enter "Cats-PracticeMt" in the box to the right of Mt:. Click on the "Cyclify" button (immediately above the large text box).   [ Show me ] Click on the "Ask Query" button (immediately above the Mt : text box).   [ Show me ]

You should see the following:

Ask a Query
   [Skip to Inputs]

Last query in Cats-PracticeMt :
(isa Billy SpatialThing)

Query halted because : Search space was exhausted.

Query was proven True   [Explain]

Yes, Cyc does know that Billy is a spatial thing! How does Cyc know this?

Try it yourself! Enter this into your copy of OpenCyc.    Click on the link "Explain" (immediately above the line that separates the result of the query and the tools for asking another query).   [ Show me ]

This useful tool should produce the following:

Inference Answer Detail   [Refresh]   [Continue Ask]
-------------------------------------------------------
Query in Cats-PracticeMt :
(isa Billy SpatialThing)

One Justification :
:ISA   (isa Billy SpatialThing) in Cats-PracticeMt 

"ISA:" is what is known as an HL module, a specialized inference-performing module of which Cyc has a great many. Clicking on it provides a summary of the particular inferences the module performed in this case.

Click here for suggested reading on this topic   Tutorial lesson on Inference in Cyc

Try it yourself! Enter this into your copy of OpenCyc.    Click on the link "ISA:", under One Justification :.   [ Show me ]

You should see the following:

HL Support Detail   [Refresh]
---------------------------------
Strength : Default   Module : ISA

Mt : Cats-PracticeMt
HL Formula : 
(isa Billy SpatialThing)

Justification : 
(isa Billy Animal) in Cats-PracticeMt
(genls Animal AnimalBLO) in BiologyMt
(genls AnimalBLO BiologicalLivingObject) in BiologyVocabularyMt
(genls BiologicalLivingObject ComplexPhysicalObject) in BaseKB
(genls ComplexPhysicalObject PartiallyTangible) in BaseKB
(genls PartiallyTangible TwoOrHigherDimensionalThing) in BaseKB
(genls TwoOrHigherDimensionalThing SpatialThing) in BaseKB

Now, just out of curiosity, let's ask if Billy is a person, and see what happens. (What would you expect to happen?)

Try it yourself! Enter this into your copy of OpenCyc.    Click on the Back button on your web browser. This should take you to the Inference Answer Detail page. Click on the link "Continue Ask" in the upper right hand corner.   [ Show me ] This will bring up the Ask a Query page. Enter "(isa Billy Person)" in the large text box.   [ Show me ] Click on the "Cyclify" button (immediately above the large text box).   [ Show me ] Click on the "Ask Query" button (immediately above the Mt : text box).   [ Show me ]

You should see the following:

Ask a Query
   [Skip to Inputs]

Last query in Cats-PracticeMt :
(isa Billy Person)

Query halted because : Search space was exhausted.

Query was not proven

Why didn't Cyc say that this statement was false?

The Cyc inference engine never returns "false" -- but only "true" or "not proven" -- as the answer to a query.

In fact the Cyc inference engine never returns false - only true or not proven. Cyc knows a great deal but has sufficient humility not to assume that its failure to prove an assertion P is a sound basis for concluding that P is false. However, let's try asking (not (isa Billy Person)) , i.e. "Is it not the case that Billy is a person?"

Try it yourself! Enter this into your copy of OpenCyc.    Scroll down below "Query was not proven" on the "Ask a Query" page. The query we just asked is still entered into the fields there. Insert "(not" just before "(isa Billy Person)" and add another ")" at the end of the query, so that you have "(not(#$isa #$Billy #$Person))" entered in the large text box. Click on the "Cyclify" button. Click on the "Ask Query" button.

You should see this proven True! Why is this? Click on the link "Explain"....and again click on the link to the ISA: inference module.

Try it yourself! Enter this into your copy of OpenCyc.    Click on the link "Explain" (next to "True" and immediately above the line that separates the result of the query and the tools for asking another query).   [ Show me ] From the "Inference Answer Detail" page, click on the link "ISA:", under One Justification :  [ Show me ]

You should see something that looks like this:

HL Support Detail   [Refresh]
---------------------------------
Strength : Default   Module : ISA

Mt : Cats-PracticeMt
HL Formula : 
(not 
   (isa Billy Person))

Justification : 
(isa Billy DomesticPet) in Cats-PracticeMt
(genls DomesticPet DomesticatedAnimal) in HumanActivitiesMt
(genls DomesticatedAnimal NonPersonAnimal) in DomesticBreedsVocabularyMt
(disjointWith Person NonPersonAnimal) in BiologyMt

This provides a summary of the inferencing which the :ISA inference module went through in this case. Can you see what went on? Basically, it followed the genls hierarchy from the collection #$DomesticPet (which Billy belongs to) up to the collection #$NonPersonAnimal . It then found an assertion that the collections#$Person and #$NonPersonAnimal are 'disjoint' - i.e. they have no instances in common (which makes sense, given their names). The module then concluded that since Billy is a member of the collection#$NonPersonAnimal , he cannot be a member of the collection #$Person .

Note that it is not the case that every query which returns "Not Proven" can be made to return "True" when negated. Consider, for example, (isa Billy Dog) . Try asking this both with and without a (not ...) surrounding it.

Try it yourself! Enter this into your copy of OpenCyc.    Click on the Tools link in the left corner of the top frame. This will bring up the "Browser Tools" page. Click on the "Ask" link in the column on the left. This will bring up the "Ask a Query" page. Enter "(isa Billy Dog)" in the large text box. Click on the "Cyclify" button (immediately above the large text box). Enter "Cats-PracticeMt" in the text box next to "Mt :". Click on the "Ask Query" button (immediately above the Mt : text box).

Try it yourself! Enter this into your copy of OpenCyc.    Click on the Tools link in the left corner of the top frame. This will bring up the "Browser Tools" page. Click on the "Ask" link in the column on the left. This will bring up the "Ask a Query" page. Enter "(not (isa Billy Dog))" in the large text box. Click on the "Cyclify" button (immediately above the large text box). Enter "Cats-PracticeMt" in the text box next to "Mt :". Click on the "Ask Query" button (immediately above the Mt : text box).

It turns out that Cyc cannot prove that Billy is or is not a dog. Cyc does not know enough about Billy to decide either way. Of course if Cyc knew that Billy were a cat then perhaps Cyc could decide this question. Remember that we did not manage to assert that Billy and Peter were cats because there was no#$Cat constant. And of course, the relevant inference would only go through if such a constant were intelligently ontologized.

If you would like to, go ahead and create a constant #$Cat (a collection, of course), assert that Billy and Peter are instances of it, make whatever assertions on it you think are required to capture the meaning of 'cat' and, in particular, make whatever #$disjointWith assertions are required for Cyc to be able to prove that Billy is not a dog. (Make sure you test with an actual 'Ask' to verify!)

Now, if you are up to a challenge, see if you can make whatever #$disjointWith assertions are required for Cyc not to conclude any analogous wrong thing about Billy....:-)

Click here for suggested reading on this topic   Further reading on negation in CycL

What else should we expect Cyc to be able to infer about Billy and Peter?

Here are some suggestions for further Asks:

  • Is Billy light enough to be carried around? (Can be proven True, under the right circumstances)

  • Have Billy and Peter ever met or come into physical contact? (Can be proven True, though this one is harder than the last! Hint: the relevant predicate may take some digging up.)

I encourage you to try doing some other asks, then making some other assertions, then doing still further asks....You are now on your way to becoming a Cyc-savvy ontologist. Have fun!!

Now that you hav completed the shorter versions of steps three and four, if you would like a more detailed explanation of how to use microtheories and where to place assertions in the microtheory hierarchy, then read the considerably longer version of this walkthrough.

Step four summary - we have performed some inference-testing and found out that Cyc does not only know what we told it in Step 3, it is able to make certain inferences based on that knowledge, which shows that it has integrated that knowledge into the larger KB.