HANNIBAL: An efficient tool for logic verification based on recursive learning. This paper introduces a new approach to logic verification of combinational circuits, which is based on recursive learning. In particular, the described method efficiently extracts equivalencies between internal nodes of the two circuits to be verified. We present a tool, HANNIBAL, which is very efficient for many practical verification problems where such internal equivalencies exist. The presented method can also be used to drastically accelerate other verification tools. Experimental results clearly show the efficiency of HANNIBAL. For example, HANNIBAL verifies the multiplier c6288 against the redundancy-free version c6288nr in only 48 s on a Sparc Workstation ELC.