CycL: The Cyc Knowledge Representation Language

CycL is Cyc's large and extraordinarily flexible knowledge representation language. It is essentially an augmentation of first-order predicate calculus (FOPC), with extensions to handle equality, default reasoning, skolemization, and some second-order features. (For example, quantification over predicates is allowed in some circumstances, and complete assertions can appear as intensional components of other assertions.)  CycL uses a form of circumscription, includes the unique names assumption, and can make use of the closed world assumption where appropriate.
For more information, see the detailed description of CycL language features.