Cyc is constructed using a form of FirstOrderLogic with support for non-monotonic reasoning and contexts, as described by JohnMcCarthy (1993). The open source version of Cyc is available at http://www.opencyc.org/

In the CycKnowledgeBase (KB), information is partitioned into contexts or 'MicroTheories' such that any formula is represented in the form ist(C, P) where C is a context (microtheory (Mt)) and P is a proposition. An inheritance structure allows more specific contexts to inherit general information from outer contexts, but they can have information that is inconsistent with other MicroTheories outside of their InheritanceHierarchy. Thus we might have something like the following:

                BaseKB
          _________|____________
         |                      |
 NaivePhysicsMt          QuantumPhysicsMt

where some knowledge represented in NaivePhysicsMt is inconsistent with QuantumPhysicsMt, but both share all knowledge in BaseKB. Mc''''''Carthy proposed that such inconsistent information could be re-formulated and introduced into the sister context by use of LiftingRules. 
-----
Some claims made at the CycOrg Web Site:

From this point forward, real-world CommonSense can be expected to play an integral part of software applications. For the first time, the world's only large-scale, task-independent, language-independent, extensible, reusable, common-sense knowledge base is being made available to the world. Beginning now, software can become increasingly and arbitrarily smarter.

As of 20020817, there were three Public Servers listed, only one of which could be reached. There were twenty or so users on a 333Mhz machine and time for screen updates ran into the minutes. More on this later.

Some elaboration might make this page more valuable.

''A real-world example of Cyc being used would also be valuable.''
----

http://cyc.com/ and http://opencyc.org/ (the commercial effort released a subset as an open source ontology). This is a knowledge base that tries to capture CommonSense; as such some aspects of psychology are supposed to be in its expert system. Again, I am not exactly endorsing the effort, but it is certainly worth knowing about; it is unique. The brainchild of DougLenat. 

The Suggested Upper Merged Ontology (SUMO) is also a resource worth considering, since all of its axioms are freely available. SUMO is one of the largest and most comprehensive, free, formal ontologies. It includes a full set of manually created links to the WordNet? lexicon. The main site for SUMO is http://www.ontologyportal.org. There are also many free domain ontologies built on SUMO, and an open source browsing and inference system called Sigma. SUMO has been expressed both in KIF and OWL. 
----

See also: CycMergedOntology
----
CategoryArtificialIntelligence