Formal reasoning in intelligent database systems

摘要

Expert database systems were proposed to solve the difficulties encountered in traditional database systems. Prolog provides a fast prototyping tool for building such database systems. However, an intelligent database system implemented in Prolog faces a major restriction that only Horn rules are allowed in the knowledge base. We propose a theorem prover which can make inference for non-Horn intelligent database systems. Conclusions can be deduced from the facts and rules stored in a knowledge base. For a knowledge base with a finite domain, the prover can provide correct answers to queries, derive logical consequences of the database, and provide help in detecting inconsistencies or locating bugs in the database. The theorem prover is efficient in deriving conclusions from large knowledge bases which might swamp most of the other deductive systems. The theorem prover is also useful in solving heuristically the satisfiability problem related to a database with an infinite domain. A truth maintenance mechanism is provided to help eliminate repetitious work for the same goals.