How a Constant is Presented

The assertions involving #$TeethCleaning are organized into several sections some of which already will appear in the right frame, but all the sections may be found by following their links in the left frame:


This section includes documentation and system-related assertions, such as those using #$comment and #$myCreationTime.

Definitional Info

Assertions that most fundamentally define #$TeethCleaning's role in the KB are listed in this section. This includes #$isa and #$genls assertions. When the browser displays predicates or functions, their arity and argument types also go in this section.

Lexical Info

This section contains lexical information, including any #$denotation links and part-of-speech information.

Applicable Relations

All predicates which can apply to the displayed constant (via some argument) are displayed here. That is, the constant meets the argNisa (where N is currently 1-5) constraint of the relation.

All Assertions

This section has a complete listing of all assertions which involve the displayed constant. The total number is listed in parentheses.

All GAF's

This section lists all ground atomic formulas (GAF's) involving the displayed constant. The number of GAF's that will be displayed is given in parentheses.

Arg: 1Arg: 2, etc.

In the Arg: 1 section, #$TeethCleaning is the first argument in each assertion; in the Arg: 2 section, it is the second argument, and so on.

Predicate Extent

This section applies only to relations. Clicking on this link will display all assertions in which the displayed constant is in the 0th argument position (e.g., (constant x y)). Since #$TeethCleaning is not used as a predicate, you won't see this link.


Here, the displayed constant appears in axioms that use #$implies. In these rules, the constant appears in the antecedent of the rule.


In this section, the displayed constant appears in the consequent of the #$implies rules.

Microtheory Contents

This section is only available if the displayed constant is a #$Microtheory. Since #$TeethCleaning is not a #$Microtheory, you won't see this section here. All assertions in the microtheory may be displayed by selecting this link.


This section contains all other references to the displayed constant that are not covered in the previous categories.

Other links in the left frame may appear as subcategories within some of these main categories. These links work mainly as would be expected, by refining those things displayed in the main categories. For instance, predicate names may appear under Arg 1, and clicking on the predicate names will display uses of that predicate that contain the displayed constant in the Arg 1 position. If microtheories appear as subcategories, then clicking on it will display the same items as the main category, but restricted to only those assertions that are in that microtheory.