1. 2

I added the compsci tag because automated theorem proving is discussed.

  1.