Cyc is more than a just database of facts about the world. It also contains the ability to reason with these facts (and data), answering questions or producing conclusions that require the appropriate combination and integration of its explicit knowledge. The Cyc inference engine is responsible for producing these results in an effective and efficient manner.
Cyc's inference engine performs general logical deduction (including modus ponens, modus tollens, and universal and existential quantification), with AI's well-known named inference mechanisms (inheritance, automatic classification, etc.) as special cases. Cyc performs best-first search over proof-space using a set of proprietary heuristics, and uses microtheories to optimize inferencing by restricting search domains.
Because the Cyc KB contains hundreds of thousands of assertions (aka "rules"), many approaches commonly taken by other inference engines (such as frame-based expert system shells, RETE match, Prolog, etc.) just don't scale up to KBs of this size. As a result, Cycorp has invested years of R&D effort to create a hierarchically-controlled, highly tunable, self-improving, and extremely modular reasoning architecture. Rather than taking a one-size-fits all approach, Cyc contains many (currently over a thousand) special-purpose inferencing modules for handling a specific classes of inference and types of problems. For instance, one such module handles reasoning concerning collection membership/disjointness, while others handle equality reasoning, temporal reasoning, and mathematical reasoning.