I heard theorem proving is a hard problem, hard enough that it contributed to an early AI winter. But how hard?
While reading about proof assistants, I have come to realize that there are many types of theorem proving/logic behind: propositional logic, first-order (FOL), high-order (HOL), various type theories, and many others maybe.
My question is:
What are the computational complexity (roughly speaking) for theorem proving for the different types of logic behind theorem provers?
(e.g. undecidable, NP-hard, polynomial time etc.)
I just wanted to get a rough idea.