THING is the class of everything in the universe of discourse that can be in a class. This includes all the relations and objects defined in the KIF specification, plus all other objects defined in user ontologies. Every THING is either a simple-set or an individual.
There are entities in the universe of discourse for KIF that cannot be instances of THING. These entities are unbounded objects, which by definition cannot be members of any set. Since THING is a class, and classes are relations, and relations are sets, then unbounded entities can't be instances of any class.
That is why THING is defined here, as the practical root of all ontologies.
- Version 4: moved THING from the KIF ontology into the frame ontology. It isn't defined in the KIF spec, and mainly serves to clarify the relationship between sets and classes.
(=> (Individual-Thing ?X) (Thing ?X))
(<=> (Individual-Thing ?X) (And (Thing ?X) (Individual ?X)))