of a program-assisted proof is the one that shows that the game of Connect Four can always be won by the first player.

Applications

Commercial use of automated theorem proving is mostly concentrated in integrated circuit design and verification. Since the Pentium FDIV bug, the complicated floating point units of modern microprocessors have been designed