4 ms·

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 a

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). For example, this bit from https://wtgowers.github.io/human-style-atp/motivatedproofs.html https://wtgowers.github.io/human-style-atp/motivatedproofs.h...: >> 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. I think I misunderstand what are "move types" (is that the same as "proof steps" in other contexts? I don't understand those, either). 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. 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.

zozbot234 4y ago
Resolution proof does a lot of backtracking, and ends up with "unintuitive" proofs as a result. One thing that's clear enough about this project is that it's trying to avoid general search as much as practically possible.
- YeGoblynQueenne 4y ago
  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!)

zozbot234 4y ago

Resolution proof does a lot of backtracking, and ends up with "unintuitive" proofs as a result. One thing that's clear enough about this project is that it's trying to avoid general search as much as practically possible.

YeGoblynQueenne 4y ago
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!)