>> This is of course correct as far as it goes, but it's not what this project means by "motivation" of a proof. Their concept of "motivation" is a lot closer t

>> This is of course correct as far as it goes, but it's not what this project means by "motivation" of a proof. Their concept of "motivation" is a lot closer to "what would your reasoning process be if you were trying to derive the proof yourself". In particular, this requires avoiding needless brute-force searches. (It's probably the case that some statements can only be proven via brute-force, but if so they're of course out of scope for a project aiming for "motivated" proofs!) Hm, I don't know if I would characterise the search in SLD-Resolution (or anyway its implementation in Prolog) as a "brute force" search. To clarify, search in SLD-Resolution is used to find clauses whose heads unify with a goal and not to find proofs, or parts of proofs. It is also naturally implemented as a depth-first search because that happens to match well with the selection rule (basically, "always go left"). But Resolution in effect comes with its own "pruning" in that as the proof proceeds the resolution closure gets smaller and smaller, and so does the search space. There is also SLG-Resolution that basically switches semantics to breadth-first search and avoids left-recursions. So the search is not brute force and dumb, like in searching a game tree. I'd say brute force in the context of finding a proof would be more along the lines of "here's a set of possible proofs, find one that works". But maybe you mean the backtracking, when you're talking about "brute force"? Anyway I think I understand what you mean about human-like proofs, essentially. I think that's a completely different goal and motivation than actually finding actual proofs. In a sense, if I can draw an analogy to gaming again, it would be like trying to find a theory of chess, or go, that would work as a closed-form solution, instead of having to minimax and MCTS all the game trees. It's a more classic AI motivation: how do humans think (in this case, how do they prove things?) and why? That's a great kind of motivation, if I'm right, and I fully understand its value. On the other hand, I think there's also great value in being able to mechanise the "boring" parts of a proof -and they are boring, if they can be automated away! - and letting the human brain do what it does best, which is express its ideas in a formal language. Resolution theorem-proving is great for this. Thanks for the explanation. I think I get it a bit more now :)