The NVL knowledge representation language

Semantic networks are described by means of a formal relational logic called NVL. The characteristic features of this logic are limiter lists and binary predicates. Limiter lists are similar to restricted quantifiers but are more expressive. Use is made of several special binary relations to express the key ideas of semantic networks. The formal semantics of NVL is specified, and the soundness of the axioms and inference rules is proved. Parallel algorithms for unification and inference are also developed. The unification and inference mechanisms of NVL have considerable inherent parallelism, which makes the language suitable for parallel implementation. NVL is based on the structured representation of knowledge and is hence more efficient than predicate logic. However, unlike other knowledge representation languages based on semantic networks, NVL has a clean, formal semantics which eliminates the confusion about what a sentence in the language really means