Knowledge Interchange Format
Knowledge Interchange Format (KIF) is a language designed to be used for exchange of knowledge between different systems. It is based semantically on predicate logic and syntactically on LISP. It allows representing arbitrary sentences in the first order predicate logic. This language was defined within the Ontolingua project that provides a cooperative ontology builder that allows exporting ontologies to various formalisms.
When KIF is used, one usually implements a representation formalism in KIF and uses this implementation for representation of particular ontology or knowledge. This is also the case of Ontolingua - Frame Ontology defining classes, slots, facets etc. was defined in KIF, and the KIF together with the frame ontology forms the language of Ontolingua, that allows write ontologies in a canonical form. These ontologies can then be exported to other formalisms, such as Prolog. Even when KIF was primarily intended as interlingua, it is currently used for encoding knowledge directly. Other formats may be exported from KIF definition automatically (see for example SUMO).
For example, KIF definition expressing that a rail vehicle is a vehicle designed to move on railways is written as:
(subclass RailVehicle LandVehicle) (documentation RailVehicle "A Vehicle designed to move on &%Railways.") (=> (instance ?X RailVehicle) (hasPurpose ?X (exists (?EV ?SURF) (and (instance ?RAIL Railway) (instance ?EV Transportation) (holdsDuring (WhenFn ?EV) (meetsSpatially ?X ?RAIL))))))
Since KIF is highly expressive to be able to serve as an interchange format between various knowledge representation formalisms, it is not surprising that no reasoning support has ever been provided within Ontolingua.