FORMAL REASONING IN INTELLIGENT DATABASE-SYSTEMS

Expert database systems were proposed to solve the difficulties encoun tered in traditional database systems. Prolog provides a fast prototyp ing tool for building such database systems. However, an intelligent d atabase system implemented in Prolog faces a major restriction that on ly Horn rules are allowed in the knowledge base. We propose a theorem prover which can make inference for non-Horn intelligent database syst ems. Conclusions can be deduced from the facts and rules stored in a k nowledge base. For a knowledge base with a finite domain, the prover c an provide correct answers to queries, derive logical consequences of the database, and provide help in detecting inconsistencies or locatin g bugs in the database. The theorem prover is efficient in deriving co nclusions from large knowledge bases which might swamp most of the oth er deductive systems. The theorem prover is also useful in solving heu ristically the satisfiability problem related to a database with an in finite domain. A truth maintenance mechanism is provided to help elimi nate repetitious work for the same goals.