So far this document has dealt mostly with the syntax of sentences in CycL. This is the syntax used by people or external programs when they assert things into a version of the CYC KB or query the KB. Now we will shift our focus to what sentences look like once they have been asserted into the KB.
The CYC KB consists of a large number of assertions. When a sentence is successfully asserted into the KB, it is stored as one of these. Each assertion is composed of a number of elements:
- a sentence
- a microtheory
- a truth value
- a direction (or access level)
- a support
We’ll discuss each of these and point out where they come from. It’s important that you be familiar with all of them:
You are already familiar with sentences–they are the CycLSentence-Assertibles we use to state things in the CYC KB.
Every assertion is contained in some microtheory. A particular sentence may be asserted into (or concluded in) more than one microtheory; when this is the case, there will be an assertion which has that sentence in each of those microtheories. The largest number of assertions are currently in the #$BaseKB.
Microtheories are covered in more detail here, as well as in the constant vocabulary, under #$Microtheory. Where does the microtheory information on assertions come from? That depends on the origin of the assertion. If an assertion is added to the KB by the inference engine as the result of firing a rule, the inference engine code decides what microtheory the conclusion should be added in and records it at add time. If an assertion is the result of a person or external program asserting a sentence into the KB, at that time the asserter must specify which microtheory the sentence is to go in. Some interfaces for knowledge entry may not require the user to specify a microtheory for new assertions, and will then either try to choose the right one or will use #$BaseKB as a default. If you use such an interface make sure you know what the default behavior is, because the BaseKB is usually far too general a place for new knowledge.
Attached to every assertion is a truth value that indicates its degree of truth. CycL contains five possible truth values, of which the most common are default true and monotonically true.
Assertions that are monotonically true are held to be true in every case, that is, for every possible set of bindings to the universally quantified variables (if any) in the assertion, and cannot be overridden. In the case of a monotonically true assertion with universally quantified variables in its sentence, if an object is found for which the assertion is not true, an error is signalled. In the case of a ground assertion that is monotonically true, if the negation of that sentence is ever asserted or arrived at during inference (in the same microtheory), an error is signalled.
Assertions that are default true, in contrast, are held to be true in most cases, and can be overridden. If the negation of an existing ground, default assertion is asserted in the same microtheory, or is arrived at through inference, no error is signalled. Instead, the argumentation mechanism is invoked to decide what the final truth value of the assertion will be.
By default, GAFs which begin with the predicates #$isa and #$genls are monotonically true, while all other assertions (including rules) are default true.
Direction is a value associated with every assertion that determines when inferencing involving that assertion should be performed. There are three possible values for direction: forward, backward, and code. Inferencing involving assertions with direction forward is performed at assert time (that is, when a new assertion is added to the KB), while inferencing involving assertions with direction backward is postponed until a query occurs and that query allows backward inference. By default, GAFs have direction forward, while rules have direction backward. Only in very special cases should rules have direction forward.
Assertions with direction code are not used in normal inference at all; instead, special HL modules have been written to supplant the need for inference using the assertion itself, and the assertion remains in the KB for documentation purposes only. Code assertions cannot be edited via the HTML interface.
One way of viewing directions is as a hierarchy of “when it gets used” :
- Assertions declared :code are exhaustively supported directly by HL modules.
- Assertions declared forward are used exhaustively in forward inference. All :code assertions are also used implicitly at this level since the HL modules supplanting them are used here.
- Assertions declared backward are only used in backward inference. All :forward assertions are also used at this level, and the HL modules supplanting :code assertions are again used at this level.
Attached to every assertion is a support, which consists of one or more justifications which form the support for the presence of the assertion in the KB. In many cases, at least one of the supporting justifications is local, indicating that the assertion was added to the KB from an outside source (most commonly, a human KEer). In other cases, a supporting justification is a source which indicates the assertion was inferred and which outlines the final step of some argument, or chain of reasoning, which supports the assertion.
The support is the one element of an assertion which need not be specified by the KEer when performing knowledge entry. It is created and updated automatically. However, supports can be displayed by KB browsing tools.