>> If you take an 8x8 chessboard and remove any
  >> black square and any white square, the resulting
  >> mutilated chess-board is guaranteed to be exactly
  >> coverable by dominoes, each of which covers exactly
  >> two squares. We can program a computer to conduct
  >> an exhaustive search to show that this is true.
  >> Would you consider the program to be an automated
  >> reasoner?
	
  > Yes,

That surprises me. That feels a lot like describing Eliza as a conversationalist. Technically true, but ultimately unhelpful and unenlightening.

By way of contrast with the above described brute-force search, which also only works on a fixed size board, here's a proof that works on all NxN boards, where N is even.

We can construct a tour of the squares, visiting each exactly once, each time moving from a square to one of the squares with which it shares a side. Removing one black and one white divides this into two (or possibly only one) segments. Each can easily be shown to be of even length, and therefore each is coverable by dominoes. QED.

If you simply enumerate a very large number of possibilities, it doesn't feel like reasoning.