Glossary

argument / arg

A term in a CycL expression of the CycL expression of the form (Arg0 Arg1 ... ArgN). ArgN refers to the term in the Nth position, with the first term being Arg0 which is distinguished as the predicate position.  e.g., in the CycL expression (#$genls #$Dog #$CanineAnimal), Arg0 is #$genls, Arg1 is #$Dog, and Arg2 is #$CanineAnimal.

argument

A belief or a deduction that supports an Assertion (a particular #$CycLAssertion), i.e., is the basis for (or against) that Assertion being true. An Assertion is supported by either the fact that it was directly asserted to the KB was created by one or more applications of a rule assertion.  Each instance of #$CycArgumentDatastructure is either a #$CycDeductionDatastructure or an #$HLAssertedArgumentKeywordDatastructure.

arity

AThe number of arguments a predicate or function takes or that a formula has.  e.g., #$genls requires two arguments, so (#$arity #$Genls 2).

ask

A facility for querying the KB, obtaining bindings for variables in CycL EL formulas, rr obtaining confirmation that a ground formula is present in the KB.

assert

A facility for inputting facts and rules into the KB. Also known as Tell in the KB literature.

assertion

A semantically well-formed CycL sentence (#$CycLSentence) that is present in the KB either through direct input by a Cyclist or as a result of inference from other assertions.  If it was directly asserted to the KB, it is a CycLAssertedAssertion; else it is a CycLDeducedAssertion. (Note that a given Assertion may be both, since it can be both explicitly asserted and deduced.)

atomic term

A term in a CycL expression that is not constructed from other CycL terms.  Atomic terms may be a #$CycLConstant, a #$CycLVariable, or a #$SubLAtomicTerm.

backward inference

On-demand query-driven reasoning where existing assertions and rules are applied to satisfy a user- or applcation-posed goal.

body

In Lisp macros, the body is a sequence of statements which define the expansion of the macro call into an evaluatable Lisp expression.

characterp

A predicate function which returns T if and only if the single argument is a character type.

closed

Not containing any free (i.e., unbound) variables.

collection

A kind or type of thing whose instances share a certain property, attribute, or feature.  e.g., #$Cat is the collection of all, and only, cats.

constant

A unique symbol within the KB.  Al l#$CycLAtomicTerms other than #$CycLVariables and #$SubLAtomicTerms are constants. e.g., '#$Dog' and '#$genls' are CycL constant, while other CycL terms such as '?X', '42', and '(#$GovernmentFn #$France)' are not.

CycL

The declarative language of the Cyc system in which assertions are written. CycL is derived from first-order predicate calculus, but includes many extensions to FOPC which enhance the expressiveness of the language.

deduced assertion

A Cyc data structure containing one or more supports which, taken together, provide some support in favor or against a given KB assertion. Also known as a Justification in the KB literature.

deduction

An assertion supported by at least one argument which is a deduction by Cyc's inference engine (as opposed to having been explicitly asserted to Cyc).

denotational term

CycL terms that are not a #$CycLSentence, i.e., terms that are either #$CycLAtomicTerms or #$CycLNonAtomicTerms.

direction

An inference attribute of an assertion. Value :forward means that at the time of assertion, the inference engine uses the new assertion with all existing rules in applicable microtheories to derive additional assertions. Value :backward means that the the inference engine may use the new assertion to derive assertions when seeking bindings for an Ask operation. Rules default to :backward because they may otherwise potentially generate many uninteresting assertions. GAFs default to :forward because forward inference serves to derive likely useful additional assertions in a limited manner.

EL

An acronym for Epistemological Level which is a CycL representation optimized for human authoring and understanding. The canonicalizer facility of the KB automatically translates input formulas in EL form into efficient Heuristic Level (HL) representation. Likewise an uncanonicalizer facility generates EL formula from their HL counterpart representation. For example the logical operator #$implies is used at the EL, but the KB converts implications to Conjunctive Normal Form (CNF) at the HL.

expression

A Cyc constant, variable, or formula (i.e. non-atomic terms and sentences).  Each CycL expression is, trivially, a syntactically well-formed expression of CycL, but note that it might or might not be semantically well-formed.

FI

An acronym for the Functional Interface which is a small set of powerful high-level API functions that support constant/assertion creation in, and removal from, the KB, as well as queries.

formula

A CycL expression that denotes a relation (e.g., a #$Predicate, #$Function-Denotational, or #$TruthFunction)  followed by one or more CycL terms, with the entire sequence enclosed in parentheses.  For example, (#$isa #$Muffet #$Poodle) and (#$BirthFn #$Muffet) are both CycL formulas.  Two important specializations of #$CycLFormula are #$CycLNonAtomicTerm (whose instances are also called "denotational formulas") and #$CycLSentences (whose instances are also called "logical formulas").

FORT

An acronym for First Order Reifiable Term, i.e., constants, NARTs, etc. (as opposed to higher-order terms such as sentences or propositions).

forward inference

Eager application of KB rules triggered by the addition of a new assertion or rule to the KB.  Conclusions reached by forward inference are asserted to the KB which may, in turn, trigger additional forward inference.

free variable

A variable in an expressino that is not bound, i.e., is not inside the scope of a quantifier or othe rscoping relation.

fully ground expression

A CycL expressino that contains no variables, free or bound.

function

A specialization of #$Relation that is a mapping from one of a set of thigns (the functions #$relationDomain) to another set of things (its #$relationRange).

GAF

An acronym for Ground Atomic Formula which is an assertion without any variables (i.e., ground) and without logical connectives (i.e., atomic). GAFs form the great majority of KB assertions. The Arg0 term in a GAF is the predicate.

genl

A CycL predicate meaning the generalization relationship of a specific KB collection to a more general collection.

formula

A formula is an expression following CycL syntax.

fort

An acronym for First Order Reified Term which is defined to be either a constant or a Non-Atomic Reified Term (NART).

function

In the API context, this is a either a built in SubL procedure or one defined using SubL definition facilities.

HL

An acronym for Heuristic Level which is the efficient interal representation of KB datastructures and the procedures for accessing them.

hypothesize

A feature of the KB which allows a query to be answered by automatically instantiating any required constants.

id

A unique integer identifier for a KB item.

iff

If and only if.

indexed term

Those terms, arguments to CycL predicates or functions, which are suitable for indexing in the KB. The great majority of KB terms are indexed. Non-indexed terms are primarily logical connectives, heavily used CycL predicates having alternate efficient access mechanisms, and unlikely query candidates such as numbers.

individual

A Cyc term that is not a set or collection. Individuals might be concrete or abstract, and include (among other things) physical objects, events, numbers, relations, and groups.

isa

A CycL predicate meaning membership in a collection.

KB

An acronym for Knowledge Base, the corpus of information modeled in Cyc.

map

A SubL function which applies an argument SubL function over a set of objects, either to return a result or for a side-effect purpose.

macro

A SubL source code expansion facility.

microtheory

An atemporal, aspatial, informational thing that represents a context in Cyc. Each microtheory (or 'mt') serves to group a set of assertions together that share some common assumptions; the assertions in an mt constitute the content of that mt. Note that each assertion in the Cyc knowledge base must be explicitly stated to be true in at least one microtheory. Assertions stated to be true in one mt will also be true (by inference) in more specialized mts that depend on the content of that mt. Note that every query is made in some mt, and the answer one gets to a query depends on the mt in which it is asked, since the only assertions which can be used to answer a query in an mt are those explicitly stated to be true in that mt, or in some more general mt.

mt

A acronym for Microtheory.

nart

A Non-Atomic Reified Term is a CycL term (argument to CycL predicate or function) which is neither a variable nor an atomic (one word) constant. NARTs are are terms formed by applying a CycL function to its arguments.

ontological engineering (OE)

The practice of creating and managing formally knowledge models (e.g., an ontology), especially formal representations of a set of concepts and their inter-relationships.

open

An expression is "open" if it contains one ore more free variables.

OWL

An RDF/XML-based ontology authoring language.

predicate

A CycL predicate generally conveys relationships that may hold between constants, such as #$capitalCity in the expression (#$capitalCity #$UnitedStatesOfAmerica #$CityOfWashingtonDC).  The predicate appears in the Arg0 position.

prove

A KB query returning a list of supporting arguments for the given formula, if it can be proven within the specified resource constraints.

reified

A term for which there is an indexed data structure in the Cyc KB.

rule

A CycL formula containing variables whose EL representation begins with #$implies. A rule has two parts, called its antecedent (left-hand side) and consequent (right-hand side).

search space

When performing a query operation, the search space denotes all the possible derived assertions, obtaining the total number of bindings for the query. The inference engine explores the search space, seeking bindings in an efficient fashion, limited by the given resource constraints.

sense

At the HL, sense distinguishes either the positive (via :pos) or negative (via :neg) clauses of an assertion represented in Conjunctive Normal Form.

sentence

A CycL expression comprising a #$TruthFunction (e.g., a #$Predicate or #$SententialRelation) followed by one or more Cyc terms, with the entire sequence enclosed in parentheses, e.g., '(#$isa #$Collection #$Thing)' or '(#$genls ?FOO #$SpatialThing)'.

string

A SubL object consisting of a sequence of characters.

SubL

A Lisp-like programming languaged used as a primary programming language for Cyc.

support

A KB support is circumstance (represented by a variety of HL datastructures) affecting the belief in a particular assertion. Supports are linked to assertions via KB arguments.

strength

An assertion may have strength values from among the following: :default (true unless otherwise as an exception known to be false), :true (true because a user specifies it absolutely true), :unknown (truth value cannot be determined at this KB state).

term

A syntatically well-formed expression in the CycL lanaguage that can be combined with other expressons to form non-atomic terms or formulas.

tms

An acronym for Truth Maintenance System. The KB facility whereby previously derived assertions are automatically unasserted when KB supports are removed. TMS ensures a consistent KB when a supporting assertion is undone by the user.

trie

An ordered tree data structure used by Cyc for efficient storage and access of certain types of information, especially strings used for certain Natural Language Processing functions.

truth

An assertion may have either the value :true or the value :false as its truth value. The great majority of KB assertions have truth value :true.

truth value

A composite assertion attribute for strength and truth attribute combinations. The truth value :true-mon means absolutely true. The truth value :true-def means true unless otherwise known to be false. The truth value :unknown means that the truth value is not known to be true and not known to be false. The truth value :false-def means false unless otherwise known to be true. And :false-mon means absolutely false.

variable

A type of CycL term appearing in rules standing for not-known-in-advance constants that satisfy the formula of a rule. When used in a KB query, variables specify which bindings are sought by the inference engine. Variables are character strings whose initial character is a question mark ("?").

well-formed

When referring to a formula, conforming to rules regarding the number and types of arguments.