KM is a powerful, frame-based language with clear first-order logic semantics. It contains sophisticated machinery for reasoning, including selection by description, unification, classification, and reasoning about actions using a situations mechanism. Its origins were the Theo language and the (now obsolete) language KRL. It is implemented in Lisp.
The DART (Discovery and Aggregation of Relations in Text) database contains approximately 23 million distinct "world knowledge" propositions (110 million with duplicates), extracted from text by abstracting parse trees. The extraction system (DART) is based on ideas by Len Schubert. The DART system and database is described in detail in the paper below. The database was generated from the Reuters and BNC corpora. The database was created by Peter Clark and Phil Harrison (Boeing Research and Technology) and is publically available under the GNU Lesser General Public Licence.