1. A method used in a computer, comprising: providing a logical theory ( 12 , 30 ) having clauses; generating a rule ( 14 ) that is a resolvent of clauses in the logical theory; retrieving an example ( 16 ); generating a proof tree ( 18 , 40 ) from the example ( 16 ) using the logical theory ( 12 , 30 ); transforming the proof tree ( 18 , 40 ) into a database ( 20 , 42 ) of a coverage check apparatus ( 28 ); converting the rule ( 14 ) into a partial proof tree ( 60 ) having nodes ( 62 , 54 , 66 ); transforming the partial proof tree into a database query ( 22 ) of the coverage check apparatus ( 28 ); and executing the query ( 22 , 72 ) to identify tuples in the database ( 20 , 42 ) that correspond to the nodes of the partial proof tree.