A Network-based knowledge representation and its natural deduction system

We describe a knowledge representation scheme called K-NHT and a problem solving system called SNIFFER designed to answer queries using a K-NET knowledge base. K-NtT uses a partitioned semantic net to combine the expressive capabilities of the first-order predicate calculus with linkage to procedural knowledge and with full indexing of objects to the relationships in which they participate. Facilities are also included for representing taxonomies of sets and for maintaining hierarchies of contexts. SNin-TR is a manager and coordinator of deductive and problem-solving processes. The basic system includes a logically complete set of natural deduction facilities that do not require statements to be converted into clause or prenex normal form. Using SN'II tFR's coroutine-based control structure, alternative proofs may be constructed in pseudo-parallel and results shared among them. In addition, SNitf ER can also manage the application of specialist procedures that have specific knowledge about a particular domain or about the topology of the K-NER structures, for example, specialist procedures are used to manipulate taxonomic information and to link the system to information in external data bases.