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 (12, 30) that has clauses. A rule (14) is generated that is a resolvent of clauses in the logical theory. An example (16) is retrieved. A proof tree (18, 40) is generated from the example (16) using the logical theory (12, 30). The proof tree (18, 40) is transformed into a database (20, 42) of a coverage check apparatus (28). The rule (14) is converted into a partial proof tree (60) that has nodes (62, 54, 66). The partial proof tree is transformed into a database query (22) of the coverage check apparatus (28). The query (22, 72) is executed to identify tuples in the database (20, 42) that correspond to the nodes of the partial proof tree.