Assertion Display Frame Help
E-Mail Comments to: opencyc-doc@cyc.com
Copyright© 1997-2002 Cycorp. All rights reserved.
See the Key for Icons in the Browser for an explanation of icons used in this section.
The Assertion Display Frame displays the details of a single CYC® assertion, and allows the user to perform a number of operations on that assertion.
Assertions in the KB are uniquely identified by an assertion ID number. This is listed at the top of the page. If the assertion is public (i.e., contains only public constants), the word public will appear to the left of the assertion ID.
- "Truth" lists the truth value of the assertion, which can be True, False, or Unknown. Values of True or False will be followed by the strength of the truth value (default or monotonic).
- "Direction" lists the direction of the assertion, which can be Forward, Backward, or Code. Assertions with a direction of Code were not asserted to the KB, but rather are implemented in the SubL code, and as such cannot be edited via the Browser.
- "Arguments" lists the number of arguments that immediately support this assertion. Clicking on the link will display those arguments. This differs from Justify, which lists not only the first level of supports, but the entire chain of arguments back to local assertions or HL supports.
- "Dependents" is the converse of Arguments. It lists the number of assertions which depend upon the displayed assertion for their existence; these are the assertions which are reevaluated (and possibly deleted) if the displayed assertion is unasserted. Clicking on the "Dependents" link will display all of those assertions.
- "Mt" lists the #$Microtheory in which the assertion is true. If the same assertion is true in another microtheory as well, this is in effect a different assertion and will be listed separately under a different assertion ID.
- "HL Formula" lists the actual assertion as it is stored in the KB, if the HL form differs from the EL form. Most assertions are stored in their EL form, and thus no HL form will be listed.
- "EL Formula" lists the actual assertion in its EL form (usually the form of the rule when it was entered into the KB).
- "English Translation" provides an English version of the assertion, generated by CYC®.
- "Meta Assertions" lists (meta) assertions about the assertion, if any. If the assertion has meta assertions about it, it will be marked with a yellow "M" M.
There are a number of different operations involving assertions:
- "Change Mt" allows the user to change the #$Microtheory in which the assertion is true. This option will only appear for local assertions.
- "Change Strength" allows the user to change the strength of an assertion's truth value from Default to Monotonic and vice-versa. This option will only appear for local assertions.
- "Change Direction" allows the user to change the direction of an assertion from Backward to Forward and vice-versa. Remember that forward assertions are used in inference at assert time, while backward assertions are used in inference when a query which allows backchaining occurs. This option will only appear for local assertions.
- "Assert Similar" brings up an assertion editing window with a copy of the assertion in it as a default. The user can then modify the new copy before entering it into the KB.
- "Edit" brings up an assertion editing window with a copy of the assertion in it. The user can then modify the original assertion and commit the changes to the KB. In actuality, this causes the original assertion to be deleted, and a new but similar one to be asserted in its place. The new version of the assertion will have a different assertion ID number from the original. Attempts to reference the assertion via the old ID will not succeed. This option will only appear for local assertions.
- "Unassert" deletes the assertion from the KB, removing all of its dependents (conclusions that CYC® has drawn from it). This option will only appear for local assertions.
- "Blast" removes deduced assertions from the KB, since they cannot be unasserted. All dependents are withdrawn, but the supports that led to the assertion's being concluded will remain in the KB. Blast is most often used in conjunction with exception rules (e.g., #$exceptWhen), where an unwanted conclusion (for a specific case) is drawn from a general rule.
- "Redo TMS" forces full TMS (Truth-Maintenance) to be performed on the given assertion. Performing TMS on an assertion essentially asks the system to reevaluate all of the arguments for that assertion. This is most useful when the assertion has a deduced source which depends on an HL (Heuristic Level) support which no longer holds. Thus, if an assertion looks like it has a stale HL support justifying it, clicking on "Redo TMS" will make the stale argument go away. This link will only appear when an assertion has at least one HL support.
- "Justify" provides the justification chain for the assertion. If it's a local assertion, the Cyclist who asserted it will be cited as a source. If it's deduced, the assertions which led to its deduction will be displayed.
- "Repropagate" causes the assertion to be used in inference immediately. This is akin to reasserting a forward rule into the KB.
- "Diagnose" performs low-level diagnostics on the assertion. This is only available in certain versions of the CYC® System.
- "HL Data" displays a Heuristic Level (HL) description of the given assertion. This option is only available in certain versions of the CYC® System.
For more information about assertions and their properties (e.g., truth value), read the Syntax of CycL.
Go to Top