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 sure those sentences “make sense.”
Syntactic well-formedness is satisfied when a formula has the right numbers of arguments given to the relations used, and when the objects appearing in the formula are syntactically correct for the place they appear. For example, it would violate CycL’s syntax if a
#$BinaryPredicate were used with three arguments; if the logical connective
#$not was given more than one sentence as an argument; and if a string or integer appeared in the predicate position (immediately after an open parenthesis) of an atomic sentence. Each of those cases would be deemed syntactically ill-formed.
Semantic well-formedness is satisfied when all semantic constraints, such as those imposed by
#$strictlyFunctionalInArgs, to name only a few such constraint-imposing predicates, are satisfied.