## Glossary of Common CYC® Terminology

E-Mail Comments to: opencyc-doc@cyc.com
Last Update: 3/28/2002
Copyright© 1996-2002 Cycorp. All rights reserved.

Return to Table of Contents

This document is a glossary of jargon you are likely to encounter in the CYC documentation and in conversation with Cyclists. Important CYC Constants have their own documents, which you can find in the vocabulary section on the Table of Contents page. For a more complete list of abbreviations, see Abbreviations in CYC.

## Contents:

- access level (AL)
- antecedent
- argument
- argumentation
- arity
- ASK
- ASSERT
- asserted
- assertion
- atomic formula
- axiom
- backward
- code
- collection
- communication mode
- conditional
- conjunctive normal form (CNF)
- consequent
- constant
- constant documentation
- context
- constraint language proposition expression (CLPE)
- Cyc API
- Cyc-9
- Cyc-10
- CycL
- CycL Formula
- Cyclist
- deduction
- default
- default true
- dependents
- direction
- disjunction
- epistemological level (EL)
- existential quantification
- expression
- first-order predicate calculus (FOPC)
- formula
- first order reified terms (FORT)
- forward
- frame-based
- frame-based display
- function
- functional interface (FI)
- #$genlMt
- ground atomic formula (GAF)
- ground expression
- heuristic level (HL)
- inferred
- interval-based quantity expression (IBQE)
- individual
- inference
- justification
- knowledge base (KB)
- KEer
- literal
- local
- logical connective
- microtheory
- modus ponens
- modus tollens
- monotonic
- monotonically true
- natural language (NL)
- non-atomic term (NAT)
- NUE
- ontology
- predicate
- quantification
- quantifier
- reification
- relation
- remote
- rule
- scope
- Skolem function
- skolemization
- slot
- source
- spec
- strength
- SubL
- Sublisp
- support
- term
- transcript
- transcript server
- truth maintenance system (TMS)
- truth value
- unification
- unit
- unit of measure
- universal quantification
- variable
- well-formed

### access level (AL)

  (obs.) In Cyc-9, the access level of an assertion determines whether inferencing involving that assertion occurs at assert time or at ask time. Access level is replaced in Cyc-10 by direction.

  Only two access level values were commonly used in Cyc-9: 0, which corresponds to the Cyc-10 direction forward, and 4, which corresponds to the Cyc-10 direction backward.

  For more information on direction, click here.

### antecedent

  The antecedent of a rule is its left-hand side, that is, the first argument to the #$implies connective with which the rule begins. Intuitively, every rule states that if the antecedent is true, then the consequent must be true.

### argument

  The term "argument" is used in two different ways by Cyclists:

  - Most commonly, the term "argument" is used to refer to any CycL term which follows a predicate, a function, a logical connective, or a quantifier in a Cycl expression. Thus, in the CycL formula (#$likesAsFriend #$BillM #$Goolsbey), #$likesAsFriend is a predicate, and #$BillM and #$Goolsbey are the first and second arguments to that predicate.

  - The term "argument" is also used to refer to a reason why an assertion is present in the KB with its truth value. Arguments are of two main types: the first type of argument is essentially a statement that the formula was explicitly "asserted" (or "local"). The second type of argument is the group of assertions through which the assertion was "inferred" (in which case the assertion is called "remote"). In this case there is a chain of inference which supports the truth value of the supported assertion. Such arguments are also called deductions.

### argumentation

  Argumentation is the process of weighing various arguments, pro and con, for the truth of an assertion, and arriving at a truth value for the assertion. CYC® employs a number of heuristics during argumentation. One simple example is "prefer monotonic rules," i.e., if two rules conclude P but with different negation status (one concludes P with a monotonic rule but the other concludes Not-P with a default rule), all else being equal, CYC® sets the truth value of P to the one suggested by the monotonic rule.

### arity

  The arity of a CycL predicate or function is the number of arguments it takes.

  - Unary predicates and functions take just 1 argument.
  - Binary predicates and functions take 2 arguments.
  - Ternary predicates and functions take 3 arguments.
  - Quaternary predicates and functions take 4 arguments.
  - Quintary predicates and functions take 5 arguments.

  No CycL predicate or function currently takes more than 5 arguments.

### ASK

  The purpose of an ASK operation is to query a CYC® Server about the truth of a formula.

  The details of an ASK operation vary from interface to interface. However, in most interfaces you will be asked to supply:

  - A CycL formula, which may or may not contain free variables. If the formula contains variables, then you are asking CYC® to supply bindings to those variables which make the formula true; otherwise, you are simply asking whether the formula is true.

  - A microtheory within which to look. In other words, each binding returned must come from a formula which is known to be true in, or can be inferred from assertions in, the specified microtheory and its baseMts.

  - Optionally, a direction (or access level). If the direction is forward, no expensive inferencing is performed, and the only bindings returned are ones which can be found through a simple KB lookup. If the direction is backward, inferencing is performed.

  - Optionally, a number of bindings requested. Once this number of bindings has been found, the ASK operation will terminate, even if more bindings exist. The default value varies among interfaces; if no value is passed by the interface on to the underlying code, the operation will continue until one of the other resource limits has been reached or until the KB has been exhaustively searched, which could take a long time.

  - Optionally, a time limit. No more than this many seconds will be spent on the ASK operation. Again, a particular interface may provide a default time limit, but if none is passed to the underlying code, the ASK operation will continue until one of the other resource limits has been reached or until the KB has been exhaustively searched.

  - Optionally, a inference depth cutoff. The search for bindings will go no deeper than this number of levels. In the search for bindings, each time the inference engine tries to satisfy a literal, the search is extended by one depth level. Currently, this is true whether literals are satisified by firing rules or by simple KB lookup. If no inference-depth cutoff is passed by your interface on to the underlying code, the ASK operation will continue until one of the other resource limits has been reached or until the KB has been exhaustively searched.

  - Optionally, an axiom depth cutoff. No more than this many rules will be used in the search for bindings. If no axiom-depth cutoff is passed by your interface on to the underlying code, the ASK operation will continue until one of the other resource limits has been reached or until the KB has been exhaustively searched.

  For example, if you wanted to find some people who have served as head of state of a European country, you might execute an ASK with the following parameters:

         Formula:         (#$and
                             (#$geographicalSubRegions #$ContinentOfEurope ?X)
                             (#$headOfStateOf ?X ?Y))
         Microtheory:     #$BaseKB
         Direction:       backward
         Number:          5
         Time:            10
         Inference Depth: 10
         Axiom Depth:     3

  This asks CYC® to find no more than 5 bindings for ?X and ?Y, satisfiable in the #$BaseKB, that can be found in 10 seconds of processor time or less. CYC® can use rules in the search, since the direction is backward, and can stop pursuing any search path as soon as it requires using a 4th rule or satisfying an 11th literal.

### ASSERT

  The purpose of the ASSERT operation is to add a new assertion--a "fact" or a "rule"--to the KB. If an ASSERT operation is successful, afterwards the KB will contain one or more new assertions.

  The details of an ASSERT operation vary from interface to interface. However, in most interfaces you will be asked to supply:

  - A CycL formula, which is either a rule or a GAF. If the ASSERT is successful, and the formula can be internally represented as a single assertion, the new assertion will have a formula logically equivalent to this one. If the formula requires several assertions to represent it, the conjunction of the formulas of the new assertions will be logically equivalent to the formula asserted.

  - A microtheory within which to put the new assertion(s).

  - Optionally, a direction. If the direction is :backward, the new assertion(s) can participate in backward inference only. If the direction is :forward, they can participate in both forward and backward inference. Because of this, asserting a forward formula may cause other formulas to be added to the KB at that time as forward inference kicks in.

    If the direction is :CODE, the new assertion(s) will not be used during normal inference at all. Default values for direction vary among interfaces, but if none is passed on to the underlying code, the new assertion will have :forward if it is a GAF, and :backward if it is a rule.

  - Optionally, a strength. Possible strengths are :default and :monotonic. This value, together with whether the formula is negated (begins with #$not) or not, determines the truth value of the resulting assertions when an ASSERT operation succeeds.

    The default value for strength is nearly always :default.

### asserted

  An asserted assertion is one that was explicitly added to the KB via an ASSERT operation. An "asserted argument" is an argument claiming an assertion was asserted. Contrast with inferred.

### assertion

  The assertion is the fundamental unit of knowledge in the CYC® system. Every assertion consists of:

  - a CycL formula which states the content of the assertion
  - a truth value
  - a microtheory of which the assertion is part
  - a direction (in Cyc-9 this was an access level)
  - a justification

  The set of assertions includes both rules and GAFs.

### atomic formula

  An atomic formula is an expression in CycL of the following form: a list with opening and closing parentheses such that the first element of the list is a CycL predicate, and the remaining elements are the arguments to the predicate. Atomic formulas use no logical connectives. See also ground atomic formula. In CycL atomic formulas may have variables, constants, or other terms as arguments to the CycL predicate.

### axiom

  Strictly speaking, an axiom is one of a set of fundamental formulas that one starts with to prove theorems by deduction. In CYC®, the axioms are those formulas that have been locally asserted into the CYC® KB. CYC® axioms are well-formed CYC® formulas, since the system won't let you add formulas to CYC® that are not well-formed. However, not all well-formed CYC® formulas are axioms, since not all of them are actually in the KB. And some of the formulas in the KB are not, strictly speaking, axioms, since they were added to the KB via inference, instead of being locally asserted.

  In informal usage, though, Cyclists don't always adhere to the strict meaning of axiom, and may refer to a formula they are considering adding to the KB or have recently removed from the KB as an axiom.

  Axiom is also the name of one of the internal KB data structure types.

### backward

  "Backward" is one of the possible values for direction that an assertion may have. If an assertion is :backward, it may participate in backward inference only.

  "Backward" also refers to a mode of inference where rules do not fire until the user ASKs some formula that triggers a rule.

  See also forward and code.

  Backward inference example: If the user asks "What things are green?":

         (#$colorOfObject ?X #$GreenColor)

  this would trigger a rule in the KB that says "All leaves are green":

      RULE 1:
         (#$implies
           (#$isa ?LEAF #$Leaf)
           (#$colorOfObject ?LEAF #$GreenColor))

  Then if CYC® can find something that is a leaf (like #$Leaf0037), thus satisfying the antecedent of the rule, it fires the rule, adding

         (#$colorOfObject #$Leaf0037 #$GreenColor)

  to the KB and returning #$Leaf0037 as a binding for ?X. In backward inference, CYC® doesn't bother finding something to satisfy the antecendent of RULE 1 until a user or application program does an ASK of some formula that in part matches the consequent of RULE 1.

### code

  "Code" is one of the possible values for direction that an assertion may have. If an assertion is :code, then special HL modules have been written to supplant the need for inference using the assertion itself. Code assertions cannot be edited via the HTML interface.

  "Code" can also refer to the SubL source code.

  See also backward and forward.

### collection

  In CycL, collections are denoted by certain constants which are called "collection-denoting" constants. These are often referred to as "CycL collections" or just "collections" in casual usage. CycL collections are constants that denote collections of objects, rather than individual objects. For example, the constant #$Dog denotes the collection of all dogs, while the individual-denoting constant #$Snoopy denotes a specific dog. For more on this topic, see the constants #$Collection and #$Individual.

### communication mode

  The communication mode controls how a CYC® Server communicates with other CYC® servers about operations performed on the CYC® KB. All communication between CYC® servers occurs via transcripts. For more information about transcripts and communication modes, click here.

### conditional

  A conditional is the same thing as a rule.

### conjunction

  Conjunction is represented in CYC® by the CycL logical connective #$and. A CycL formula is sometimes called a conjunction if it begins with #$and.

### conjunctive normal form (CNF)

  A formula in CycL or first-order predicate calculus is in conjunctive normal form if it is a conjunction of disjunctions of literals. For example,

         (#$and (#$or (#$not (#$isa ?C #$Cloud))
      	        (#$colorOfObject ?C #$WhiteColor)
                      (#$colorOfObject ?C #$GreyColor))
                (#$or (#$not (#$isa ?C #$Cloud))
      	        (#$physicalStructuralAttributes ?C #$Puffy)))

  is in conjunctive normal form. For every CycL or FOPC formula, there is a logically equivalent formula that adheres to CNF.

  When a formula is asserted to CYC®, it is first converted into conjunctive normal form. For each disjunction in the resulting CNF expression, a new assertion is created. Some formulas convert to a CNF expression with only one conjunct (and therefore only one disjunction); for example,

         (#$isa #$Kermit #$Frog)

  converts to

         (#$and (#$or (#$isa #$Kermit #$Frog)))

  and

         (#$implies
            (#$isa ?FROG #$Frog)
            (#$colorOfObject ?FROG #$GreenColor))

  converts to

         (#$and (#$or (#$not (#$isa ?FROG #$Frog))
      	        (#$colorOfObject ?FROG #$GreenColor)))

  These formulas, if asserted, would result in a single new assertion being added to the KB. Other formulas convert to CNF expressions with multiple conjuncts. For example,

         (#$implies
            (#$isa ?C #$Cloud)
            (#$and (#$or (#$colorOfObject ?C #$WhiteColor)
      		   (#$colorOfObject ?C #$GreyColor))
                   (#$physicalStructuralAttributes ?C #$Puffy)))

  converts to

         (#$and (#$or (#$not (#$isa ?C #$Cloud))
      	        (#$colorOfObject ?C #$WhiteColor)
                      (#$colorOfObject ?C #$GreyColor))
                (#$or (#$not (#$isa ?C #$Cloud))
      	        (#$physicalStructuralAttributes ?C #$Puffy)))

  This last formula, if asserted, would result in two separate assertions being added to the KB, one for each conjunct.

### consequent

  The consequent of a rule is its right-hand side, that is, the second argument to the #$implies connective with which the rule begins. Intuitively, every rule states that if the antecedent is true, then the consequent is true.

### constant

  Constants are terms introduced into CycL by explicit creation. Constants such as #$BillM or #$likesAsFriend begin with "#$". Constants are one type of FORT; the other type are non-atomic terms (NAT's). For more on the syntax and usage of constants, click here.

### constant documentation

  Documentation strings for constants, in, or accessible from, the KB.

### constraint language proposition expression (CLPE)

  This is an old name for a Cyc formula.

### context

  Often used interchangeably with microtheory.

### Cyc API

  The CYC® API is an applications programming interface that allows programmers to build applications based on the CYC® technology. Click here for more information about the Cyc API.

### Cyc-9

  The last version of CYC® developed at MCC.

### Cyc-10

  The current version of CYC® developed at Cycorp under the direction of Keith Goolsbey, and first deployed there in March, 1995. All current CYC® development effort is with Cyc-10.

### CycL

  CycL is the formal language in which CYC® assertions are written. CycL derives from first-order predicate calculus, but includes many extensions to FOPC which enhance the expressiveness of the language. For a more complete description of CycL syntax, click here.

### Cyclist

  A Cyclist is a registered modifier of the CYC® KB. Everyone who works on the CYC® project is a Cyclist, as are individuals working with CYC® at participating organizations.

### CycL Formula

  A formula is an expression in a formal language that makes some declarative statement about the world. Formulas are analogous to declarative sentences in English. In CycL, formulas that are well-formed are called CycFormulas. For more information about the syntax of CycFormulas, click here.

### deduction

  A deduction is an argument supporting a remote or inferred assertion. It is composed of a set of assertions which together entail the inferred assertion.

### default

  One of the possible values for strength. If a formula is asserted with a strength of :default, the resulting assertion(s) will have a truth value of either default true or default false, depending on whether or not the asserted formula was negated. Default rules can have exceptions, and default GAFs can have their truth values changed by argumentation. See also monotonic.

### default true

  An assertion which is default true is assumed to be true in all cases, unless there is evidence to the contrary. Thus, unlike an assertion which is monotonically true, it admits exceptions. Default true is one of CycL's five possible truth values. It is represented in the CYC® Web Interface by a yellow ball .

### dependents

  An assertion's dependents are assertions which have some deduction> (inferred argument) mentioning it. When an assertion is deleted, its dependents must be examined to see if they should also be removed.

### direction

  Direction is a value attached to every assertion which determines whether inferencing involving the assertion is done at assert time or at ask time. There are three possible values for direction: :forward (inferencing done at assert time), :backward (inferencing done at ask time), and :code (HL module performs reasoning, assertion not used in regular inference). Most interfaces enforce the following default: GAFs have direction :forward and rules have direction :backward. Direction is new in Cyc-10; it replaces access level.

### disjunction

  Disjunction is represented in CYC® by the logical connective #$or. A formula is sometimes called a disjunction if it begins with #$or.

### epistemological level (EL)

  Epistemological level refers to the way knowledge is expressed when CYC® communicates with users or external programs. This stands in contrast with heuristic level, which refers to the way knowledge is actually stored, and inference implemented, in CYC®.

### existential quantification

  Quantifying with #$thereExists. For example, the following existentially quantified assertion (#$thereExists ?SING (#$and (#$isa ?SING #$HumanAdult) (#$maritalStatus ?SING #$Single))), states that there is some unmarried human adult.

### expression

  In the most general sense, an expression is a sequence of symbols. The phrase CycL expression refers to expressions that follow the syntax rules of CycL. Some CycL expressions are propositions or statements about the world; these are called CycL formulas. Other CycL expressions form terms that stand for concepts; these are called non-atomic terms (NATs).

### first-order predicate calculus (FOPC)

  A formal language incorporating predicate symbols, function symbols, constant symbols, variables, logical connectives and quantifiers, which can be used to express facts about a world. Unlike propositional logic, FOPC can express general statements or statements about existence, by using quantified variables. "First-order" means that statements which quantify over predicate and function symbols are not allowed.

### formula

  A formula is a sentential expression in a formal language. If the expression is closed (that is, if it has no unbound variables) it can be used to express something about the world. Closed formulas are analogous to declarative sentences in English. In CycL, formulas that are well-formed are called "CycL formulas". For more information about the syntax of CycL formulas, click here.

### FORT (First Order Reified Terms)

  There are two kinds of FORTs: constants and non-atomic terms (NATs).

### forward

  "Forward" is one of the possible values for direction that an assertion may have. If an assertion is :forward, it may participate in both forward and backward inference.

  "Forward" also refers to a mode of inference where rules fire as soon as their antecedents become true.

  See also backward and code.

  Forward inference example: Suppose the KB already knows

         (#$isa #$Leaf0037 #$Leaf)

  Suppose a user or application program asserts the following as a forward rule:

         (#$implies
           (#$isa ?LEAF #$Leaf)
           (#$colorOfObject ?LEAF #$GreenColor))

  As soon as the axiom is asserted, the system detects that the antecedent is satisfied by #$Leaf0037, fires the rule, and adds the conclusion

         (#$colorOfObject #$Leaf0037 #$GreenColor)

  to the KB. Unlike backward inference, this happens automatically without needing to be triggered by an ASK operation. It also should not depend on the order in which the assertions are added to the KB: If the forward rule was added first, and it was later asserted that #$Leaf0037 was an element of #$Leaf, the rule would fire at that time.

### frame-based

  Frame-based representations attempt to collect all the information relevant to a concept on a "frame" for that concept. Each frame has a series of slots filled by values. The slots can be viewed as binary relationships between the concept of the frame, and the values filling them.

### frame-based display

  A frame-based display can present representations which are frame-based (a series of slots with values), or which are isomorphic to frames. For example, some CYC® interfaces use a frame-based display method for showing the binary predicates the displayed concept is a first argument to.

### function

  A function (in the mathematical sense) is a relation such that for each thing in its domain (the universe of things it can be applied to), there is a single thing in its range (the universe of results it can have) such that the relation holds between them. In CycL, functions are denoted by certain constants. These constants are referred to as "function-denoting constants, "CycL functions," or sometimes just "functions." CycL functions can be applied to arguments to form non-atomic terms, which can serve as arguments to a predicate just as other terms can. There are more details about CycL functions in the Functions section of "The Syntax of Cycl".

### functional interface (FI)

  The FI is an applications programming interface containing several dozen standard calls to CYC® which can be used by programmers to build applications based on the CYC® technology. The FI is a subset of a larger programming interface, the CYC® API. Click here for an index to information about the Functional Interface.

### #$genlMt

  One microtheory is a #$genlMt of another if all its assertions are true in the other microtheory. #$BaseKB is a #$genlMt of all microtheories.

### ground atomic formula (GAF)

  A GAF is a CYC® formula of the form (predicate arg1 [arg2 ...argn]), where the arguments are all terms of any kind, but not variables. For example,

         (#$likesAsFriend #$Goolsbey #$Brandy)
         (#$eats #$BillM (#$FruitFn #$AppleTree))
         (#$beliefs #$BillM (#$likesAsFriend #$Goolsbey #$Brandy))

  GAFs are a subset of atomic formulas. They are those atomic formulas in which no variables appear.

### ground expression

  An expression is ground iff it contains no variables.

### heuristic level (HL)

  Another name for this might be "implementation level". Heuristic level refers to the way knowledge is actually stored, and inference implemented, in CYC®. This stands in contrast to the Epistemological Level (EL), which refers to the way knowledge is expressed when CYC® communicates with users or external programs.

### inferred

  A adjective used to describe the type of argument consisting of a set of assertions which together entail some other assertion. Inferred arguments are also called deductions.

### interval-based quantity expression (IBQE)

  In Cyc-10, quantities like "5 dollars", "10 seconds", and "300 kilometers" are expressed using IBQEs.

  An IBQE is a special kind of non-atomic term in which the CycL function is an instance of #$UnitOfMeasure. Units of measure are regular (but not reifiable) functions, which take two arguments: a minimum value and a maximum value. The second argument is optional, and if it is omitted, it is assumed to be equal to the first. In other words, an IBQE with just one argument is taken to denote a single value.

         (#$massOfObject #$BillM (#$Pound-UnitOfMass 175 185))
         (#$heightOfObject #$BillM (#$Inch 74))

  The unit of measure may be a NAT, rather than a constant:

         (#$massOfObject #$BillM ((#$Kilo #$Gram) 80 84))

### individual

  In the CYC® ontology, an individual-denoting constant is a constant hat denotes a single object, rather than a collection of objects. For example, the constant #$Snoopy denotes a specific dog, while the collection-denoting constant #$Dog denotes the collection of all dogs. Sometimes individual denoting CycL contants are casually referred to as "individuals." For more on this topic, see the constants #$Individual and #$Collection.

### inference

  Inference is the process of automatically adding new facts to a knowledge base by applying rules of inference to the axioms and already-inferred facts of the knowledge base. CYC® currently uses two rules of inference in its general theorem proving, modus ponens and modus tollens.

### justification

  A justification is the argument or set of arguments supporting an assertion's having a particular truth value.

### KEer

  Short for Knowledge Enterer. One who writes CycL assertions for inclusion in the CYC® KB.

### knowledge base (KB)

  The CYC® KB is the repository of Cyc's knowledge. It consists of a large number of FORTs and an even larger number of assertions involving those constants.

### literal

  Most generally, a literal is a CYC® expression of the form (predicate arg1 [arg2 ... argn]), or its negation, where the number of arguments to the predicate can be any positive integer (but usually not more than 5), and the arguments can be any kind of term. For example,

         (#$likesAsFriend #$Goolsbey #$Brandy)
         (#$eatsWillingly #$BillM (#$FruitFn ?X))
         (#$isa ?CAR #$Automobile)
         (#$performedBy ?ACT ?ORG)
         (#$not (#$performedBy ?ACT ?ORG))

  Because it includes negated formulas, the class of literals is a superset of the class of atomic formulas.

  Usually, "literal" is used to refer to the atomic formulas that make up the internal representation of any assertion's formula. In Cyc-10, formulas that are asserted into the KB are converted into conjunctive normal form; the formula of each single assertion is internally represented as a disjunction of literals. Those literals that would be negated in conjunctive normal form are called negative literals; the rest are called positive literals. GAFs are the subset of positive literals in which there are no variables.

### local

  Old term meaning "asserted".

### logical connective

  Logical connectives are represented in CycL by special constants that are similar to the logical operators of formal logic. CycL connectives (as these constants are sometimes called) are used to build up complex formulas out of atomic formulas. The CycL constants representing the logical connectives are #$not, #$and, #$or, and #$implies. For more details on the syntax of CycL connectives, click here.

### microtheory

  A microtheory is a CYC® constant denoting assertions which are grouped together because they share a set of assumptions. Microtheories are also called contexts. For more information about microtheories, see #$Microtheory or click here.

### modus ponens

  A rule of inference under which, given a knowledge base which contains the formulas "A" and "A implies B", one may conclude "B".

### modus tollens

  A rule of inference which can be derived from modus ponens under which, given a knowledge base which contains the formulas "Not B" and "A implies B", one may conclude "Not A".

### monotonic

  One of the possible values for strength. If a formula is asserted with a strength of :monotonic, the resulting assertion(s) will have a truth value of either monotonically true or monotonically false, depending on whether or not the asserted formula was negated. Monotonic rules may never have exceptions, and monotonic GAFs will never have their truth values changed in the course of argumentation. The only way a monotonic assertion can be removed from the inference playing field is by unasserting it. See also default.

### monotonically true

  An assertion which is monotonically true is asserted to be absolutely true in all cases. Thus, unlike an assertion which is default true, it does not admit exceptions. Monotonically true is one of CycL's five possible truth values. It is represented in the CYC® Web interface by a white ball .

### natural language (NL)

  Natural language is just human language, for example English. When people talk about "NL" aspects of CYC®, they are referring to Cyc's growing ability to understand natural language.

  For a discussion of Cyc's NL capabilities, click here.

### non-atomic term (NAT)

  A term which is neither a variable nor a constant. NATs are terms formed by applying a function to its arguments. Like constants, each NAT denotes some thing in the Cyc KB. Currently, there are two kinds of NAT: Reified NATs, which are a type of FORT, and are implemented with data structures that have indexing allowing all uses of the NAT to be retrieved; and non-reified NATs, which have no such indexing and remain in the form of a "lispy" expresion in the formulas in which they occur.

  For more details on the syntax and usage of NATs, click here.

### ontology

  In philosophy, ontology is the study of being. In knowledge-based systems, an ontology is that part of the system which specifies what things exist and what is true about them. Cyc's ontology is essentially its whole knowledge base. You may hear people refer to their "ontology of devices" or their "temporal ontology". What they are talking about is those parts of their knowledge base (the constants and assertions) that concern devices or time.

### predicate

  Predicates are represented in CycL by constants that are sometimes referred to as "CycL predicates" or, more casually, as "predicates." Like CycL functions (the other kind of relation-denoting constants), CycL predicates can be used as the leading term (after the initial parenthesis) in CycL expressions. When a CycL predicate is applied to the right number and type of arguments, the expression formed is a CycL formula--a formula expressing a proposition about something. In contrast, expressions formed with functions as arg 0 (in the leading position) are terms and so do not express propositions.

  By convention, constants that denote predicates begin with lowercase letters.

  For more information about the syntax and use of predicates in CYC®, click here.

### quantification

  Quantification is a way to talk about objects without being specific about the identity of the objects involved. There are two kinds of quantification: existential and universal. Each quantification uses one quantifier and one variable. For details on quantification, click here.

### quantifier

  A quantifier is a special type of CYC® constant used in quantification. CycL contains five quantifiers: #$forAll, #$thereExists, #$thereExistAtLeast, #$thereExistAtMost, and #$thereExistExactly. Each quantifier introduces a new variable.

### reification

  To reify something is to create a CYC® FORT corresponding to that thing, or in other words, it is to add a thing that denotes it to Cyc's knowledge base. Cyclists commonly use the term "reify" in two slightly different ways:

  - Reifying a concept refers to the manual creation of a CYC® constant to denote that concept.

  - Reifying a NAT refers to the automatic preservation in the CYC® ontology of FORTs corresponding to non-atomic terms that use elements of #$ReifiableFunction. For more on this topic, click here.

### relation

  In Cyc® "relation" is informally used to refer to predicates and functions. In the math or database worlds, a relation is a set of ordered n-tuples. One might talk about the relation "Father", whose elements include (Katherine, Lloyd), (Karen, Wes), (John, Bob), and so on, where the first item in each element is a person and the second is that person's biological father. CycL relations are also ordered n-tuples. The notation we use is different from that above and depends on whether the relation to be represented by a CycL function or a CycL predicate. In both cases, we reify a constant to stand for the relation. In our example, we might call the constant #$FatherFn -- an uppercase name, because the relation is a function (people have only one biological father). We'd write, for example

         (#$FatherFn #$Katherine)

  to refer to Lloyd, since Katherine and Lloyd are in the "Father" relation.

  CycL predicates are the other main sort of relation-denoting constant in CYC®. The latter are used to represent relations which are not functions (not single-valued). The relation denoted by "parents" should be represented with a CycL predicate. For example, we'd write

         (#$parents #$Katherine #$Lloyd)
         (#$parents #$Katherine #$Bonnie)

  to say that (Katherine, Lloyd) and (Katherine, Bonnie) are in the parents relation. The arity of CycL predicates is the same as the arity of the represented relation, and the arity of CycL functions is one less than the arity of the relations they represent.

### remote

  An old term meaning inferred.

### rule

  Informally, a rule is any CycL formula which begins with #$implies, that is, any conditional. A rule has two parts, called its antecedent and consequent, or left-hand side and right-hand side.

### scope

  The scope of a quantifier is the range in which its corresponding variable is bound. It begins with the left parenthesis which precedes the quantifier, and ends with the matching right parenthesis.

### Skolem function

  Skolem functions are CycL functions which are used in the implementation of formulas that use existential quantification. They are instances of #$ReifiableFunction, and are automatically generated. For more information about skolem functions, click here.

### skolemization

  This refers to the practice of implementing formulas that use existential quantification by replacing existentially quantified variables with special terms that use skolem functions and are a function of the other variables in the rule. It can also refer to what happens when one of these rules fires: a new constant is generated, or "skolemized". For more information about skolemization, click here.

### slot

  A slot is simply a CycL binary predicate such as #$startingDate. Historically, the name derives from the days when CYC® was a frame-based system. People will sometimes speak of a slot on a certain constant, or of a constant having slots. One might say, for example, that the constant #$BillM has a #$likesAsFriend slot, or that #$likesAsFriend is a slot on #$BillM. This signifies only that there is some GAF in the KB having #$likesAsFriend as its predicate and #$BillM as its first argument.

### source

  An old word for argument.

### spec

  "spec" means "subset". In Cyc-8, there was a predicate called #$spec, which was the inverse of #$genls. The predicate became obsolete in Cyc-9, but Cyclists still use it all the time when talking about the CYC® ontology. For instance, one might say, "#$Deity is a spec of #$Agent."

### strength

  Strength is one of the components of truth value, which is a property of every CYC® assertion. Its possible values are :default and :monotonic.

  At the epistemological level, specifically, when the user is ASSERTing a formula to CYC®, strength is one of the parameters that must be specified. At the heuristic level, i.e., once assertions are stored in the KB, strength is subsumed by truth value, which is a combination of strength and whether or not the original formula was negated.

### SubL

  SubL stands for SubLanguage, and is a computer language created by the CYC® team. It is designed to be easy to translate into C. The entire CYC® application is written in SubL.

### Sublisp

  An archaic term for SubL.

### support

  A support is a justification.

### term

  A term is anything that can be an argument to a predicate or function. Variables are terms. Constants, both atomic constants and reified NATs, are terms. Non-reified NATs are terms. Numbers, strings, or even entire formulas can serve as terms.

### transcript

  A transcript is a file which records operations performed on the CYC® KB. At a site where several copies of CYC® are in use simultaneously (such as the Austin office in early 1996), transcripts are used to keep the various copies of the KB synchronized with each other. For more on the functioning of the transcript mechanism, click here.

### transcript server

  An application separate from the Cyc® program which is used at sites having multiple, collaborating Cyc® installations. The transcript server serializes operations from multiple machines and keeps them up-to-date on transmitted (i.e. shared) operations.

### truth maintenance system (TMS)

  A truth maintenance system is a mechanism whereby a knowledge based system can keep reasonably consistent and truthful as its knowledge changes. For example, if facts have been added to the KB through inference based on a set of premises, and one of the premises is later removed from the KB, any conclusion that depends on that premise should also be removed from the KB. The CYC® TMS relies on the fact that each assertion has all of its arguments recorded in the datastructure.

### truth value

  In the Cyc® KB, a truth value is a value attached to an assertion which indicates its degree of truth. There are five possible truth values:

  monotonically true (100)
    True always and under all conditions. Normally reserved for things that are true by definition.
  default true (T)
    Assumed true, but subject to exceptions. Most rules in the KB are default true.
  unknown (~)
    Not known to be true, and not known to be false.
  default false (F)
    Assumed false, but subject to exceptions.
  monotonically false (0)
    False always and under all conditions.

  Of these, the most commonly used are the first two.

  Each of these truth values is represented by a different colored ball in the KB Browser. For details on the icons used in the Browser, see the Key For Icons In the Browser.

  "Truth value" is a heuristic level property; it is a combination of what is 2 separate properties at the epistemological level: strength (:default or :monotonic) and negation status (whether or not a formula begins with #$not).

  If you are unsure whether to make an assertion monotonically true or default true, go with the latter.

  For more discussion, click here.

### unification

  Unification is a procedure that compares two expressions to determine whether some set of legal substitutions exists that can make the two equal. This procedure is used in inference, to determine whether to fire a rule. For example, in forward inference, if some set of assertions in the KB match (can unify with) the antecedent of the rule, we can fire the rule.

### unit

  This expression dates from the days when CYC® was a frame-based system. In those days, every constant was a named, atomic constant, and constants were called "units". Today, Cyclists still occasionally use "unit" to refer to atomic constants.

### unit of measure

  Any instance of #$UnitOfMeasure. These are functions, like #$Meter or #$Gram, which can be applied to numeric arguments to yield quantities, like (#$Meter 9) or (#$Gram 454). The resulting expressions are called interval-based quantity expressions.

### universal quantification

  Quantifying with #$forAll. In CycL formulas, variables which are not explicitly bound by a quantifier are assumed to be universally quantified. For example,

      	(#$forAll ?LEAF (#$implies
      				(#$isa ?LEAF Leaf)
      				(#$colorOfObject ?LEAF GreenColor)))

  means that every leaf is green. But in CycL, this sentence means the same as the following sentence:

      	(#$implies
      		(#$isa ?LEAF Leaf)
      		(#$colorOfObject ?LEAF GreenColor))

### variable

  One type of term. Variables appear in CYC® rules to stand for not-known-in-advance constants that satisfy the formula of the rule. Variables also are used in formulas given to the ASK utility, to stand for the results the asker wishes to find. For more information about variables, click here.

### well-formed

  A formula in CycL is well-formed if it conforms to the syntax of CycL and passes all the restrictions on arity and argument types of the relations that are used in it. For lots of information on what makes a formula well-formed, read these sections on predicates, complex formulas, and quantified formulas.

Go to Top