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.
1. A method used in a computer, comprising:
providing a logical theory having clauses;
providing a rule that has been derived from the clauses in the logical theory, and for which derivation of the rule is provided in form of a partial proof tree having nodes;
providing a set of examples;
providing derivations of the examples from the clauses in the logical theory in a form of proof trees;
transforming each proof tree into a database of a coverage check apparatus using a first process sequence;
transforming the partial proof tree into a database query of the coverage check apparatus using a second process sequence; and
executing the query to identify tuples in the database that correspond to the nodes of the partial proof tree.
2. The method according to claim 1 wherein the method further comprises determining whether the partial proof tree is identical to a portion of the proof tree.
3. The method according to claim 1 wherein the method further comprises investigating for each rule and each example whether the rule covers the example.
4. The method according to claim 3 wherein the method further comprises investigating whether a condition part of the rule is satisfied by the example.
5. The method according to claim 1 wherein the method further comprises making the partial proof tree more limiting than the logical theory.
6. The method according to claim 1 wherein the method further comprises concluding that the rule does not cover the example when tuples that correspond to the nodes of the partial proof tree cannot be identified in the database.
7. The method according to claim 6 wherein the method further comprises concluding that the rule does cover the example when tuples that correspond to the nodes of the partial proof tree can be identified in the database.
8. The method according to claim 1 wherein the method further comprises determining whether the tuples identified in the database are associated with a single example.
9. The method according to claim 1 wherein the method further comprises using the logical theory to describe all possible rules that may be created.
10. The method according to claim 1 wherein the method further comprises determining whether or not the query gives an empty result.