I’m not sure what exactly you’re asking. Would you like to read an in-depth survey of the present state of the art in automated theorem proving and automatic verification? Or are you interested in the fundamental question of why these problems are intractable in the great majority of really interesting cases? The former would require expert input, but the latter mostly boils down to some basic observations from the theory of computation, the foundations of math, and complexity theory.
Any such information would be appreciated, though in this post I’m primarily asking “what would be the benefits of having sophisticated tools for automatic proving and verification?”
I’m not sure what exactly you’re asking. Would you like to read an in-depth survey of the present state of the art in automated theorem proving and automatic verification? Or are you interested in the fundamental question of why these problems are intractable in the great majority of really interesting cases? The former would require expert input, but the latter mostly boils down to some basic observations from the theory of computation, the foundations of math, and complexity theory.
Any such information would be appreciated, though in this post I’m primarily asking “what would be the benefits of having sophisticated tools for automatic proving and verification?”