Answerability time is a common metric used for evaluating inference efficiency. It is defined as the time to first answer for answerable queries, and the total time for unanswerable queries.
The antecedent of a rule is its left-hand side (LHS), 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 Constraints are assertions in the KB that place syntactic and semantic conditions on the well-formedness of sentences and formulas. They are put on functions and relations and are used to restrict what can appear in each argument position of a predicate or function. Argument constraints most often take the form of #$isa (instance of) […]
The arity of a CycL relation (predicate or function) is the number of arguments it takes. It is declared in the KB with the predicate #$arity. Instances of #$UnaryPredicate and #$UnaryFunction take just 1 argument. Instances of #$BinaryPredicate and #$BinaryFunction take 2 arguments. …and so on for the other instances of #$PredicateTypeByArity Each instance of […]
An asserted argument is one of two types of arguments that can be used to justify the truth or falsity of an assertion in Cyc; the other kind of support is a deduction. An asserted argument records which user or application stated the assertion and when.
An asserted-argument assertion is an assertion which is input directly by a Cyclist or application program, and thus has an asserted argument. This is in contrast to deduced assertions, which are added as a result of inference within Cyc. Those categories of assertions are not disjoint, however, because an assertion may be supported by both […]
Assertions in the Cyc KB are similar to sentences stating facts and principles in a natural language such as English. However, each assertion has one intended meaning, and makes its context explicit. An assertion has several parts, including: a CycL sentence a Truth value a Microtheory, which is the context where that sentence with that […]
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 […]
An atomic term, represented in the Cyc Knowledge Base by #$CycLAtomicTerm, is a denotational term that cannot be composed of other terms. Constants (e.g., #$Dog), variables (e.g., ?X), and SubL atomic terms are all atomic terms. Denotational terms that are not atomic are non-atomic terms.
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 the formulas that have been locally asserted into the Cyc KB. Cyc axioms are well-formed formulas, since the system won’t let you add formulas to Cyc that are not […]
“Backward” is one of the possible values for direction that an assertion or rule may have. If an assertion has the direction “backward”, it may participate in backward inference only (not forward inference). Cf. forward assertion.
Backward inference refers to a mode of inference in which rules do not fire until Cyc is asked a query. If a rule is relevant to the query and transformation is allowed, the rule can be considered and might participate in a proof of the answer. This is in contrast to forward inference, in which […]
A binding is a temporary or contextual assignment of a value to something that does not have a fixed value, such as a variable or indexical term. When Cyc performs inference, it tries to find combinations of bindings for all the free variables in the query sentence such that the sentence is true with all of those values […]
A bundle is a directory of files that contains a standalone Cyc build, excluding additional components such as documentation and databases.
The canonicalization subsystem is sometimes referred to as “the Canonicalizer” (as is the canonicalizer proper). Taken as a whole, the canonicalization subsystem provides the language-level support for CycL. It primarily implements the conversion from EL to HL and back again. This can be thought of as analogous to compiling (and decompiling) code. The subsystem also […]
Canonicalizer may refer to: The Canonicalizer proper The Canonicalization Subsystem, consisting of the Canonicalizer proper, the WFF Checker, the Simplifier, and other modules.
The Canonicalizer proper is the main part of the Canonicalization subsystem: the part of the Cyc system that takes in EL expressions and converts them to HL expressions. Two different, but logically equivalent, CycL sentences are transformed into the same HL sentence by the Canonicalizer. On its way to being stored in the Cyc KB, […]
The closed world assumption is the assumption that if something is not provable, then it is false.
In CycL, collections are used to talk about general concepts rather than individual things. For example, in Cyc, #$Dog is the collection that contains all dogs. (In contrast, #$Snoopy is a particular dog, i.e. an instance of the collection #$Dog.) Collections are like sets except that, unlike a set, a collection can gain or lose […]
A conjunct is one term of a conjunction. For example, this conjunction has three conjuncts: (and (colorOfObject Leaf0475 GreenColor) (colorOfObject Kermit GreenColor) (or (colorOfObject DollarBill234820 GreenColor) (colorOfObject BladeOfGrass92112 GreenColor))) These three conjuncts are: (colorOfObject Leaf0475 GreenColor) and: (colorOfObject Kermit GreenColor) and: (or (colorOfObject DollarBill234820 GreenColor) (colorOfObject BladeOfGrass92112 GreenColor))
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 (CNF) 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.
The consequent of a rule is its right-hand side (RHS), 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, represented in the Cyc Knowledge Base by #$CycLConstant, are atomic terms introduced into CycL by explicit creation. Constants such as #$FishTaco or #$likesAsFriend begin with #$. Constants are one type of FORT; the other type are non-atomic reified terms (NARTs). See also Renaming Constants
The Cyc Inference Engine is an implementation of the Inference Algorithm, which tries to prove closed CycL sentences, and tries to find bindings for open variables in CycL sentences if they are present. These training modules give more information about the Inference Engine. Inference Algorithm Using the Inference Browser Inference Debugging [restrict level=”employee”][Content for Cycorp […]
A Cyc instance (also sometimes referred to as a Cyc image) is a running copy of the Cyc program. Most Cyclists doing development on the Cyc KB run one or more Cyc instances on their computers, letting them interact with Cyc.
The Cyc Knowledge Base (the KB) is a store of information, which consists of a large number of terms and an even larger number of assertions composed of those terms. Cyc constants are the most typical type of term, but other things, like strings and numbers (and even sentences themselves), are also terms in Cyc. [restrict level=”employee”][Content […]
A CycL sentence, represented in the Cyc Knowledge Base by #$CycLSentence, is a type of CycL formula that constitutes a syntactically well-formed sentence in the CycL language. Every CycL sentence consists of a CycL expression denoting an instance of #$TruthFunction (e.g. an instance of #$Predicate or #$SententialRelation) followed by one or more CycL terms, with the entire sequence enclosed in parentheses. For example, (isa Collection Thing) and (genls ?FOO SpatialThing) are both CycL sentences. Assertions are a […]
A Cyclist is someone, such as a Cycorp employee or Cyc licensee, who uses and interacts with Cyc. [restrict level=”employee”] [Content for Cycorp Employees Only] [/restrict]
The Decanonicalizer is a module in the Canonicalization Subsystem that converts HL expressions into logically equivalent EL expressions. It performs the inverse of what the Canonicalizer proper does.
A deduced assertion is an assertion which was created as a result of inference within Cyc, and not necessarily directly input by a Cyclist or application program. Directly input assertions are known as asserted-argument assertions. Deduced assertion are supported by at least one deduction. Sometimes deduced assertions are referred to as “inferred assertions” or more […]
Deduction may refer to a method by which inference is performed, or to a data structure stored in the Cyc KB. Inference method: Deduction in Cyc uses two rules of inference. The first is, “If P implies Q, and P is known to be true, then Q is also true.” The second is, “If P […]
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 has exceptions. It is represented in the Cyc Browser by a yellow ball. By default, every assertion in Cyc can be given an exception, or […]
In CycL, denotational terms, represented in the Cyc Knowledge Base by #$CycLDenotationalTerm, are terms that are not CycL sentences, and thus are either atomic terms (such as constants or variables) or non-atomic terms (also known as “NAT”s). Denotational terms are so-called, not because they all have denotations (not all of them do), but because they are in a certain sense the right kind of term for having a denotation. […]
In the context of the Cyc KB, the dependents of an assertion are those other assertions that use the first assertion in one of their supporting deductions. When an assertion A participates in a successful forward inference, a deduction data structure will be created. It points to the new assertion, D, which is a dependent […]
Direction is a value attached to every assertion which determines whether inference involving the assertion is done when an assertion is added to the KB, or done in response to a query being asked. There are three possible values for direction: :forward (inference triggered by the addition of a new assertion), :backward (inference done in […]
A disjunct is one term of a disjunction.
Disjunction is represented in Cyc by the logical connective #$or. A formula is sometimes called a disjunction if it begins with #$or.
Disjunctive Normal Form (DNF) is the form into which each Cyc assertion or query can be recast at the HL level. This is most salient for Cyc with respect to queries, as each query is translated into its disjunctive normal form prior to looking for bindings to the variables in the queries. For non-logicians: this […]
English-0 representations are simple natural language expressions of facts or rules to be represented in Cyc. The process of generating English-0 representations typically involves writing a list of 20-50 questions, in simple English, that Cyc should be able to answer after the knowledge has been represented in CycL. Answers to these questions will help drive […]
Epistemological level (EL) refers to the way knowledge is expressed when Cyc communicates with users or external programs. This stands in contrast with heuristic level (HL), which refers to the way knowledge is actually stored, and inference implemented, in Cyc.
The term evaluatable refers to a function or predicate for which some calculation is required in SubL. Some predicate might be deemed evaluatable if computing its value would be more efficient in a non-declarative language like CycL; for example, calculating the successor of a number, or compiling an ordered list from an unordered collection. If […]
Existential quantification is quantification with the #$thereExists quantifier. For example, the following existentially quantified CycL sentence states that there is some unmarried human adult: (thereExists ?SINGLE (and (isa ?SINGLE HumanAdult) (maritalStatus ?SINGLE Single))) Also see universal quantification.
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 first-order reified term or FORT, represented in the Cyc Knowledge Base by #$CycLReifiedDenotationalTerm, is a represented term in CycL that is reified in the KB. There are two types of FORTs: constants and non-atomic reified terms.
First-order logic (FOL) (also called first-order predicate calculus (FOPC)) is 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 (also known as “sentential logic”), FOL can express general statements or statements about existence, by using quantified […]
In CycL, a formula, represented in the Cyc Knowledge Base by #$CycLFormula, is a type of term that consists of a CycL expression that denotes a relation (e.g. a predicate) — or at least an expression that could be interpreted as having a relation as its semantic value — followed by one or more CycL terms, with the entire sequence enclosed in parentheses. […]
“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 inference refers to a mode of inference in which rules fire as soon as their antecedents become true. “Forward” is also 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 inference example: Suppose the KB already […]
A forward non-trigger literal is like a forward trigger literal except that what is isolated from the antecedent of a forward rule is the literal (or literals) that, though true, will not trigger the forward propagation of the rule. I.e., when a literal is asserted, if it is a forward non-trigger literal of a rule, […]
A forward trigger literal (FTL) is a literal that is found in the antecedent of a forward rule and which will cause the rule to fire when an assertion matching it is added to the KB. Normally, all the literals of a forward rule are FTLs, except literals with predicates that can’t be asserted or […]
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 at most a single thing in its range (the universe of results it can have) such that the relation holds between the two. In CycL, functions are […]
The functional interface (FI) is the SubL API to Cyc.
A functional predicate is a predicate that has at least one argument place with the following property: given any sequence of legal arguments placed in such a predicate’s other argument positions, there is at most one argument such that, when it is placed in the predicate’s functional position, the resulting formula is true.
Generalization refers to the #$genls predicate. A is said to generalize B iff (genls B A). The inverse relation is referred to as specification.
A ground atomic formula or GAF (rhymes with “staff”) 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 ThomasJefferson JohnAdams) (eats GeorgeWashington (FruitFn AppleTree)) (beliefs GeorgeWashington (likesAsFriend ThomasJefferson JohnAdams)) GAFs are a subset of atomic formulas. They are those atomic formulas […]
A ground expression is an expression which contains no variables.
A globally unique identifier (GUID) or universally unique identifier (UUID) is a 128-bit number that permanently identifies a data object in the KB. Global means that the GUID is the same across all Cyc instances. Unique means that the GUID refers to exactly one data object. Permanent means that the GUID never changes. For example, […]
Heuristic level (HL) refers to the way knowledge is actually stored, and 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. The use of HL versus EL sometimes seems to translate to “solve a problem by […]
A Heuristic Level Identifier (HL ID or HLID) is a compact string that externally identifies data objects in the KB. Heuristic Level means that the HL ID is based on the heuristic level rather than the epistemological level. Compact means that the HL ID is shorter than the GUID for the same data object. External […]
HL modules are specialized pieces of inference code designed to make inference more efficient. See also: Transformation Removal Removal modules [restrict level=”employee”] [Content for Cycorp employees only] [/restrict]
An HL support is a type of support that is a way of packaging up justifications that are either impractical or impossible to manifest. A single HL support can represent multiple justifications, sometimes numbering in the thousands or millions. Some HL supports are guaranteed to bottom out in a justification consisting of only assertions. Others […]
An indexical is an expression whose referent (or denotation) is determined by the context in which it is used. The term indexical, when used by a Cyclist, may refer to: a natural language indexical, which is an indexical expression occurring in natural language. For example, “I went to the store today” contains two (natural language) indexicals, I and today […]
In the Cyc ontology, an individual-denoting constant is a constant that 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 constants are casually referred to as “individuals.” See also Individuals and […]
Most generally, an inference is a series of reasoning steps via which a conclusion is supported by evidence. In the context of Cyc, inference is what Cyc does when it is asked a query. “Inference” also refers to a type of data structure that the Cyc inference engine uses to organize all the information it […]
The inference browser is the tool that permits Cyclists to peruse a particular inference after a query (regardless of whether the query succeeded or failed). It will present all of the inference information about the result of the query including which rules and GAFs were used, which transformations took place, which Mts were visible, the […]
The inference harness is the part of the Cyc inference engine which takes in canonicalized queries and attempts to provide proofs for them by performing Removal and Transformation. The three main parts of the inference harness are the Worker, the Tactician, and the Strategist. See also Inference Algorithm. [restrict level=”employee”] [Content for Cycorp employees only] […]
Inference parameters are the knobs and switches of Cyc inference. The settings chosen for each inference parameter control how the Cyc inference engine goes about trying to prove a query, encouraging certain methods, discouraging others, and setting limits on the resources it can use – e.g., on time, number of answers, search depth, etc. For […]
A justification is a list of supports that show why an answer was returned from an inference.
The KB Browser, also sometimes referred to as the “Cyc Browser”, is the current suite of tools that expert Cyc users use to interact with the Cyc Knowledge Base. It offers various ways of examining KB content and supporting data structures, tools for adding new knowledge, tools for querying Cyc via the Cyc Inference Engine, […]
A KB content test (KBCT or KCT) is a unit test of the Cyc inference engine. Creating KCTs Start a Cyc instance. In the browser, at the top of the page click [Query]. In the query sentence box, type a query sentence. Click [Ask Query]. Click [Save as Test]. In the Test Name field, type […]
A knowledge base is a repository of knowledge. See also Cyc Knowledge Base
Lexical assertions are those assertions that relate a Cyc term to words and phrases in some language that can be used to refer to the concept denoted by the Cyc term. For example, the assertion corresponding to this CycL sentence states that the thing denoted by #$Guitar-Electric can be referred to in English by the phrase “electric guitar”: (ist EnglishMt […]
A lifting rule is a rule with an #$ist (or #$liftTo) in the arg 0 position of the consequent literal. The purpose is to overrule the Mt placement of the conclusion with placement into another Mt, maybe found via some combination of antecedent literals.
Most generally, a literal is a CycL sentence 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 […]
Logical connectives are represented in CycL by special constants with names 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. The collection […]
A meta-assertion is an assertion about another assertion in the KB. Stated another way, a meta-assertion is an assertion having another assertion as one of its arguments. Common examples of meta-assertions are assertions made with the predicate #$salientAssertions and pragmas. For more information, see Making, Editing, and Removing Assertions.
A microtheory (Mt), also referred to as a context, is a Cyc constant denoting assertions which are grouped together because they share a set of assumptions. Those assertions are said to be “in” that microtheory, and each assertion is in exactly one microtheory (although it is possible for assertions in different microtheories to have the […]
Modus ponens is 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 is 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 is 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. See also default assertion.
An assertion which is monotonically true is true in all cases. In other words, unlike an assertion which is default true, it does not currently have exceptions. Such assertions are displayed in the Cyc Browser with a white ball. By default, every assertion in Cyc can be said to have an exception, unless it is […]
Natural language (NL) is just human language, for example English. This is in contrast to programming languages like Java. When people talk about “NL” aspects of Cyc, they are referring to Cyc’s Natural Language Processing (NLP) which includes both Cyc’s ability to generate natural language from CycL (i.e. Natural Language Generation (NLG)) and Cyc’s growing […]
A non-atomic reified term or NART (rhymes with “cart”), represented in the Cyc Knowledge Base by #$CycLNonAtomicReifiedTerm, is a non-atomic term which has been reified. NARTs are a type of FORT, the other type being constants.
A non-atomic term or NAT, represented in the Cyc Knowledge Base by #$CycLNonAtomicTerm, is a type of represented term and a type of formula that is not atomic, i.e., that is neither a variable, a constant, nor a SubL atomic term. NATs are terms formed by applying a function to its arguments. Like constants, each NAT denotes some thing in the Cyc Knowledge Base. Currently, there are two kinds of NAT: non-atomic […]
A non-atomic unreified term or NAUT (pronounced “nowt”) is a non-atomic term that has not been reified, possibly (but not necessarily) because it is unreifiable.
Ontological engineering (OE) is what ontologists do (or the product of that activity). Ontologists are sometimes informally referred to as “OEs” or “OEers”, though they are not officially engineers in the legal sense.
An ontologist (in Cyc-speak) is a Cyclist who focuses primarily on developing the Cyc Knowledge Base, aka the Cyc Ontology. Such individuals understand the structure of the Cyc KB and know how to express knowledge and queries in CycL. Thus, they know how to add new knowledge to Cyc, and how to ask questions of […]
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 the framework around which its knowledge base — consisting of axioms about the things that exist — is built. You may hear […]
An open variable is a type of variable indicated by a ? preceding its arbitrarily-chosen name, and which is not in the scope of any quantifier like #$forAll or #$thereExists — i.e. it is a variable that is not bound by a quantifier. Open variables often appear in queries where there is no explicit existential […]
In Cyc, an operation is a unit of work performed by a Cyc instance that can be recorded in a file on the local file system. Operations are typically KB modifications. That is, they will typically be either the addition of an assertion into the KB, an Unassert of an assertion, an Edit of an assertion, or the creation of a new term. Other […]
PlutoDiff is a technique that entails switching between two similar tabs/windows to attempt to visually spot a difference. It’s named after the method by which Pluto was discovered.
A pragmatic requirement (or pragma for short) is a type of meta-assertion on a rule. Pragmas state literals that must be true in order for the rule to be used in an inference. Like literals in the warrant of the rule (and unlike exceptions), pragmas are checked eagerly during inference. Pragmas are intended to provide […]
The Precanonicalizer is a (mostly) syntactic preprocessor for the Canonicalizer. It eliminates #$ELRelations by replacing them with their expanded forms by using their EL-evaluatable functions (see #$evaluateAtEL). For example, the #$DateFromStringFn convenience function is expanded here (and added back in the browser when showing dates.) Note that when checking for well-formedness we check both the […]
Predicates are represented in CycL by constants or NARTs 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 […]
A problem is an object used by the Worker to store a query under consideration by one or more inferences, as well as meta-information about that query, including: problem links expressing its logical or inferential connections to other problems tactics indicating units of inferential work that could be done or have been done etc.
Quantification is an expression of the quantity (roughly: how many?) of entities that have a property. Quantifiers — terms that express quantification — exist in natural languages (“few”, “some”, “all”) and in formal languages like CycL. For example, the difference in meaning between “{ Few / Some / Many / All } ontologists are rich” […]
A quantifier is a special type of Cyc constant used in quantification. CycL contains four quantifiers, represented in the Cyc Knowledge Base as instances of #$Quantifier: #$forAll, #$thereExists, #$forAllVars, and #$thereExistVars. Each quantifier introduces one or more new variables. #$forAllVars is shorthand for a series of nested #$forAll expressions. For example, (forAllVars (?X ?Y ?Z) […]
“Query” has been used to mean a lot of different things with regard to Cyc. Depending on context, it could mean one of: A CycL sentence intended to be asked, aka a query sentence. A CycL sentence, Mt, and list of inference parameters that are passed to the Cyc Inference Engine via a SubL function […]
When asking a query in Cyc, the query sentence is the CycL sentence that Cyc attempts to prove true or for whose open variables it attempts to find bindings.
The Query Tool is a tool in the Cyc KB Browser that is a user’s main interface to the Cyc Inference Engine. It lets the user ask a query in the form of a CycL sentence, and displays any answers that are found.
Reification in Cyc is the process by which we create a Cyc FORT corresponding to a particular concept. Or, to put it another way, reification is the process of adding a term that denotes a particular concept to the Cyc Knowledge Base. Every reified term in Cyc consists of an indexed data structure in the […]
In Cyc, “relation” (see #$Relation) is used to refer to predicates and functions. In the math and 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 […]
Removal refers to the process of solving a problem or subproblem via a removal module. Removal always strictly simplifies the problem, by providing bindings for an open problem or by proving or failing to prove a closed problem. Contrast this with transformation, which transforms a problem into one or more problems that may be more […]
Removal modules are a type of HL module used during Cyc inference to solve a query or sub-query by proving a fully-bound literal or by finding bindings for open variables. They are called “removal” modules because their successful application results in simplifying the query to be solved by removing one or more literals from it. […]
Represented terms, represented in the Cyc Knowledge Base by #$CycLRepresentedTerm, are denotational terms that are represented in CycL instead of being defined in SubL, the underlying implementation language used by Cyc. Constants, variables, and non-atomic terms are all represented terms.
Informally, a rule or conditional is any CycL assertion whose sentence begins with #$implies. Typically, a rule has two parts: an antecedent and a consequent, or left-hand side and right-hand side>. For example, (implies (isa ?BIRD FlightlessBird) (behaviorIncapable ?BIRD Flying-FlappingWings doneBy)) However, there are rule assertions which do not satisfy the above. For example, this […]
A rule macro predicate (RMP) is a predicate that is used to state a rule in a compact way that can be read more easily and supported with removal modules for more efficient reasoning. #$genls and #$relationAllExists are examples of commonly used rule macro predicates.
SBHL stands for “Subsumption-Based Heuristic Layer” (or “Level”). SBHL modules are removal modules that support efficient searches for Cyc’s most frequently used transitive predicates (#$genls, #$genlMt, and #$genlPreds), and for predicates that operate in conjunction with them (#$isa, #$disjointWith, #$genlInverse, #$negationPreds, and #$negationInverse). The body of SubL code that implements these modules is often called […]
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.
Semantic Knowledge Source Integration (SKSI) is a means of extending the Cyc KB by allowing information from structured knowledge sources — databases, triple stores, APIs — to be hooked into Cyc as if they were “external” assertions and used just like assertions in the KB. It relies on a model of both the physical structure […]
The Sentence Editor is an input device appearing in several tools in the Cyc Browser: Tools used to find, assert or edit assertions such as Find Assertion, Assert Sentence, Assert Similar, and Edit Assertion, as well as the Query Tool all have a Sentence Editor box. It allows the user to write or edit CycL […]
The Simplifier is a part of the Canonicalization Subsystem that performs very fast, mostly syntactic simplification of CycL sentences.
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. Whenever someone asserts to the Knowledge Base a sentence that contains #$thereExists (in an arg0 position), Cyc automatically creates a new instance of #$SkolemFunction and rewrites the assertion using […]
Skolemization 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.
Cyc predicates that take exactly two arguments are sometimes called slots, and the string “slot” shows up in the names of quite a few collections of binary predicates such as #$ActorSlot, #$QuantitySlot, #$FunctionalSlot, and more. This naming practice is a historical remnant of the earliest days of Cyc, during which it was a [frame-based] system. […]
Specialization is the inverse relationship to generalization. In speaking, Cyclists will often say that A specializes, or is a spec of, B if (genls A B) is true.
The Strategist is the component of the Inference Harness that performs the meta-meta reasoning. It reasons about the resource constraints and determines which Tactician or Tacticians would be best to use. Then it invokes the Tactician or Tacticians and cuts them off if they exceed their resource constraints.
Strength is one of the properties of a Cyc assertion. Its possible values are “has exceptions” and “currently exceptionless”. At the heuristic level, i.e., once assertions are stored in the KB, strength is combined with the EL truth value (negated or not) to produce 4 composite truth values: default true (true but with exceptions), monotonically […]
A structured knowledge source (SKS) is a body of data that can be accessed via SKSI. Examples include databases, triple stores, and APIs.
A subject matter expert or SME (pronounced “smee”) is, in military parlance, an expert in some kind of field. At Cycorp, the term also means someone who is not a Cyclist that we are working with to get knowledge in a specific area into Cyc. Sometimes the SME will enter the knowledge themselves. For more […]
SubL, aka SubLisp, is a variant of Common Lisp created by Cycorp, and is the computer language of the Cyc codebase. Originally, Cyc’s code was written in Common Lisp that ran on Lisp machines like those made by Symbolics. To make it straightforward to translate Cyc code into other languages, SubL was introduced. Currently, SubL […]
SubL atomic terms, represented in the Cyc Knowledge Base by #$SubLAtomicTerm, are atomic terms that are not represented terms in CycL. Rather, they are represented in SubL, the underlying implementation language of the Cyc system. “Atomic” here means not constructable from other terms via the SubL syntax. Examples include the terms 212, :NOUN, #x, and […]
A support is either an assertion or an HL support. They often appear in justifications, which are lists of supports.
A tactic is determined by the Worker. When executed, it performs one unit of inference. See also the section on tactics in the Inference Algorithm training module. [restrict level=”employee”] [Content for Cycorp employees only] [/restrict]
The Tactician is the component of the Inference Harness that is controlled by the Strategist, maintains a store of work that can be performed, and chooses among those tasks, instructing a Worker to work on them. More details can be found in the training module on the Inference Algorithm. [restrict level=”employee”] [Content for Cycorp employees […]
The Template OE tool (often referred to as the TOE tool) allows a cyclist to add or modify terms or assertions in bulk based on the results of a user-specified query. For more details, see the TOE tool training module.
A term, represented in the Cyc Knowledge Base by #$CycLTerm, is anything that can be an argument to a predicate or function. Variables are terms. 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 and connected by a Transcript Server, transcripts can be transmitted to keep the various copies of the KB synchronized with each other. See also Transcript Server
The Transcript Server (TS) performs the role of a “knowledge router”, effectively providing something akin to an RSS feed of continuous Cyc updates that are intended to be shared among Cyc instances. The TS is designed to receive, serialize (place in a canonical order), and distribute Cyc operations to facilitate collaboration between users of multiple […]
A transformation is a step in an inference in which a literal is replaced by another literal or conjunction of literals; it becomes the focal literal for which bindings are needed. These transformations occur based on a rule in the Cyc KB, relating the replaced literal to the replacing ones. For example, if we have […]
A truth maintenance system (TMS) is a mechanism whereby a knowledge-based system such as Cyc can remain 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 […]
In the Cyc Knowledge Base, a truth value is a value attached to an assertion which indicates its degree of truth. “Truth value” is a heuristic level property; it is a combination of what are 2 separate properties at the epistemological level: strength (exception status: having them, vs. not) and negation status (whether or not […]
TVA stands for “transitive via arg”. #$transitiveViaArg is one of the “transitive via arg” predicates supported by Cyc inference. These predicates are used to state that one predicate behaves transitively — in a specified argument place — with respect to a second binary predicate. The other main “transitive via arg” predicate in Cyc is #$transitiveViaArgInverse. […]
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 matches (can unify with) the antecedent […]
Universal quantification is quantification with the quantifier #$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 — wherein universal quantification is implicit for any apparently […]
In Cyc, a variable, represented in the Cyc Knowledge Base by #$CycLVariable, is a type of atomic term and a type of represented term. Each variable is a character string consisting of an initial question mark (‘?’) followed by one or more characters, where each of these latter characters is either an (upper- or lower-case) […]
In CycL, a well-formed formula or WFF (pronounced “woof”, same vowel as “foot”) is a logical formula that is syntactically and semantically valid. Well-formedness is different in CycL than in other logical representation languages. Most other representation languages have a notion of well-formedness that only implements syntactic checks. In such languages, a formula is either […]
The WFF Checker checks a given formula for syntactic as well as semantic well formedness. In other words, it checks whether something is a Well-formed formula. The WFF Checker is a part of the Canonicalization Subsystem, and is invoked when CycL sentences are asserted or edited, and when they are issued as queries, to make […]
The Worker is the component of the Inference Harness that does all the low-level work such as creating problems and links, bubbling up proofs, etc. It takes its orders from a Tactician.