by cycorpinc | Apr 12, 2021
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...
by cycorpinc | Apr 12, 2021
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...
by cycorpinc | Apr 12, 2021
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...
by cycorpinc | Apr 12, 2021
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...
by cycorpinc | Apr 12, 2021
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...