Method for efficiently checking coverage of rules derived from a logical theory

摘要

The method is used in a computer and includes the steps of providing a logical theory that has clauses. A rule is generated that is a resolvent of clauses in the logical theory. An example is retrieved. A proof tree is generated from the example using the logical theory. The proof tree is transformed into a database of a coverage check apparatus. The rule is converted into a partial proof tree that has nodes. The partial proof tree is transformed into a database query of the coverage check apparatus. The query is executed to identify tuples in the database that correspond to the nodes of the partial proof tree.