4 ms·

Resolution does a lot of backtracking, but it can be ignored if what is required is understanding how the proof proceeded. When the proof terminates (well, if i

Resolution does a lot of backtracking, but it can be ignored if what is required is understanding how the proof proceeded. When the proof terminates (well, if it does :) you can look at the completed proof tree and find a justification of the proof without having to follow the proof while it backtracks in real time. What is "general search" and why should it be avoided? I think maybe the problem is that the mechanical application of a single transformation is not justification enough for its own outcome because it's ... too simple? Or too abstract? Like defining all of arithmetic by starting from a counting axiom? Do I misunderstand?

zozbot234 4y ago
> When the proof terminates (well, if it does :) you can look at the completed proof tree and find a justification of the proof 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!) The real open question AFAICT is whether the informal examples given in this project of a "motivated proof" are actually also motivated in a formal sense. It may be that statements that can be formally shown to be "easy" to derive are limited to things we would already regard as so trivial as to be totally uninteresting. (For instance, statements of syllogistic logic are known to be very easy to prove; i.e. the computational complexity of finding such proofs is quite low, so they can be usefully applied even as one's knowledge base of "background" facts grows very large. But such proofs are also not very interesting!)
- 082349872349872 4y ago
  OK, just as a check to see if I'm following this thread: we have a theorem, wlog A implies B, and we'd like a proof. A motivated proof would say A implies foo, and foo implies bar, and bar implies B, where foo and bar are small expressions using concepts common to the theory we're working with. A searched proof would say A implies broguefleagle (so broguefleagles exist) and broguefleagle implies B, where broguefleagle is some odd expression that doesn't seem to occur anywhere else within the practise of this theory (a "rabbit out of a hat")? What have I gotten wrong?
  - zozbot234 4y ago
    This is what the project seems to give as their preferred examples, yes. (Though they also seem to think of this in terms of allowed "moves", which I think are heuristically-picked rules of inference? So they're sort of playing with something that's almost but not quite entirely unlike the usual notion of a restricted logic, chosen for computational tractability.) Of course my own view is that the more useful notion, in a general sense, is simply "a proof that's easy enough to find, not just check after the fact", which might not be exactly the same.
- YeGoblynQueenne 4y ago
  >> 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 :)
  - zozbot234 4y ago
    SLD-Resolution is not the same as Resolution in a general sense. Prolog works with Horn clauses, and satisfiability for any conjunction of Horn clauses can be solved in polynomial time. Thus, in a sense, you're right that such proofs do not involve computationally hard "brute force".

zozbot234 4y ago

> When the proof terminates (well, if it does :) you can look at the completed proof tree and find a justification of the proof 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!) The real open question AFAICT is whether the informal examples given in this project of a "motivated proof" are actually also motivated in a formal sense. It may be that statements that can be formally shown to be "easy" to derive are limited to things we would already regard as so trivial as to be totally uninteresting. (For instance, statements of syllogistic logic are known to be very easy to prove; i.e. the computational complexity of finding such proofs is quite low, so they can be usefully applied even as one's knowledge base of "background" facts grows very large. But such proofs are also not very interesting!)

082349872349872 4y ago
OK, just as a check to see if I'm following this thread: we have a theorem, wlog A implies B, and we'd like a proof. A motivated proof would say A implies foo, and foo implies bar, and bar implies B, where foo and bar are small expressions using concepts common to the theory we're working with. A searched proof would say A implies broguefleagle (so broguefleagles exist) and broguefleagle implies B, where broguefleagle is some odd expression that doesn't seem to occur anywhere else within the practise of this theory (a "rabbit out of a hat")? What have I gotten wrong?
- zozbot234 4y ago
  This is what the project seems to give as their preferred examples, yes. (Though they also seem to think of this in terms of allowed "moves", which I think are heuristically-picked rules of inference? So they're sort of playing with something that's almost but not quite entirely unlike the usual notion of a restricted logic, chosen for computational tractability.) Of course my own view is that the more useful notion, in a general sense, is simply "a proof that's easy enough to find, not just check after the fact", which might not be exactly the same.
YeGoblynQueenne 4y ago
>> 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 :)
- zozbot234 4y ago
  SLD-Resolution is not the same as Resolution in a general sense. Prolog works with Horn clauses, and satisfiability for any conjunction of Horn clauses can be solved in polynomial time. Thus, in a sense, you're right that such proofs do not involve computationally hard "brute force".