I'm familiar with a different kind of automated theorem proving than the one the article is about, resolution-based theorem proving. I am still very uncertain about the differences between resolution-based theorem proving and the kind of theorem proving in proof assistants, so there is much I don't understand from the "About" page and others in that site (and from previous readings about proof assistants).<p>For example, this bit from <a href="https://wtgowers.github.io/human-style-atp/motivatedproofs.html" rel="nofollow">https://wtgowers.github.io/human-style-atp/motivatedproofs.h...</a>:<p>>> One potential approach to making precise the notion of what I shall call
here a rabbit-free proof is to define a set of "move types" -- that is, methods of transforming a problem -- and defining a motivated proof to be one that can be generated using these move types. The idea is then to design the move types in such a way as to make it impossible to generate rabbits.<p>I think I misunderstand what are "move types" (is that the same as "proof steps" in other contexts? I don't understand those, either).<p>If I think about "transformations of a problem", with my mind stuck on resolution, all I can think of is transforming an initial formula to a new formula during a proof, by the application of one or more inference rules. But, in resolution theorem-proving, this kind of transformation can be achieved by successive applications of a single inference rule, the resolution rule. Briefly: given two clauses p ∨ q and ¬p ∨ r, resolution eliminates the contradiction p ∧ ¬p and derives the new clause q ∨ r, then continues until only the empty clause remains at which point the only logical consequence of the original theorem is a contradiction, allowing a proof by refutation. SLD-resolution, restricted to Horn goals and definite clauses is sound and refutation-complete and semi-decidable which is pretty much the best that can be done within a formal system, but the important thing is that a single inference rule, resolution, is doing all this work so the proof is straightforward to automate: even a dumb computer can just spam resolution steps until there are no more contradictions to eliminate. So I don't understand why choosing "move types" is an open problem, and why resolution can't be used to solve it. This is probably a result of my confusion and misunderstanding of what the other kind of automated theorem proving is all about in the first place.<p>I'm not trying to be smug. I really don't know what this is all about. Can anyone please explain? I'm also probably missing a lot of the necessary background on this.