-
-
(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.
-
-
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.
-
-
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 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.
-
-
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.
-
-
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.
-
-
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.
-
-
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.
-
-
The assertion is the fundamental unit of knowledge in the CYC® system.
Every assertion consists of:
The set of assertions includes both rules and GAFs.
-
-
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.
-
-
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" 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" 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.
-
-
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.
-
-
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.
-
-
A conditional is the same thing as a rule.
-
-
Conjunction is represented in CYC® by the CycL logical connective #$and.
A CycL formula is sometimes called a conjunction if it begins with #$and.
-
-
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.
-
-
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.
-
-
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.
-
-
Documentation strings for constants, in, or accessible from, the KB.
-
-
This is an old name for a Cyc formula.
-
-
Often used interchangeably with microtheory.
-
-
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.
-
-
The last version of CYC® developed at MCC.
-
-
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 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.
-
-
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.
-
-
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.
-
-
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.
-
-
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.
-
-
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
.
-
-
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 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 is represented in CYC® by the logical connective #$or.
A formula is sometimes called a disjunction if it begins with #$or.
-
-
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®.
-
-
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.
-
-
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).
-
-
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.
-
-
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 ormulas 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.
-
-
There are two kinds of FORTs: constants and
non-atomic terms (NATs).
-
-
"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 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.
-
-
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.
-
-
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".
-
-
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.
-
-
One microtheory is a #$genlMt of another if all its assertions are true in the
other microtheory. #$BaseKB is a #$genlMt of all microtheories.
-
-
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.
-
-
An expression is ground iff it contains no variables.
-
-
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.
-
-
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.
-
-
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))
-
-
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 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.
-
-
A justification is the argument or set of
arguments supporting an assertion's having a particular truth value.
-
-
Short for Knowledge Enterer. One who writes CycL assertions for inclusion in the CYC® 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.
-
-
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.
-
-
Old term meaning "asserted".
-
-
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.
-
-
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.
-
-
A rule of inference under which, given a knowledge base which contains the
formulas "A" and "A implies B", one may conclude "B".
-
-
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".
-
-
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.
-
-
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 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.
-
-
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.
-
-
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.
-
-
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 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.
-
-
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.
-
-
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.
-
-
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.
-
-
An old term meaning inferred.
-
-
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.
-
-
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 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.
-
-
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.
-
-
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.
-
-
An old word for argument.
-
-
"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 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 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.
-
-
An archaic term for SubL.
-
-
A support is a justification.
-
-
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.
-
-
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.
-
-
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.
-
-
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.
-
-
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 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.
-
-
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.
-
-
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.
-
-
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))
-
-
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.
-
-
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.