Some of the methods they list (like SAT solvers and model checkers) mostly obviate the actual proving part for simple statements. Instead you only need to input what you want to prove, and the computer attempts to find a proof or disproof. For many of the things you would want to prove in software, this is sufficient.