I do not have any background in mathematical logic, but I have studied computation and complexity theory. I have looked through some textbooks and there are distinctions between different kinds of logic (first or second order). I've gotten the impression that these automated deduction systems are useful in some domains but not others. To phrase the title question differently: is there anything a system like this cannot do (in theory) that a human can? Why?
closed as not a real question by Raphael♦ Feb 16 at 14:44
It's difficult to tell what is being asked here. This question is ambiguous, vague, incomplete, overly broad, or rhetorical and cannot be reasonably answered in its current form. For help clarifying this question so that it can be reopened, see the FAQ.