4 ms·

Thanks YeGoblynQueenne! My criticism at the time was about resolution uniform proof procedures. I was skeptical that a single procedure could prove typical

Thanks YeGoblynQueenne! My criticism at the time was about resolution uniform proof procedures. I was skeptical that a single procedure could prove typical complex mathematical theorems. Procedural embedding of knowledge was invented to overcome the limitations of resolution uniform proof procedures. Unfortunately, resolution requires flattening the structure of a mathematical propostion into clausal form thereby losing all of its structure. An important innovation of Planner was *not to require conversion into clausal form.* Instead, each Planner backward-chaining procedure is invoked by a noncompound goal. Furthermore, each Planner forward-chaining procedure is invoked by a noncompound assertion. Prolog is a subset of Planner in which a Prolog procedure is invoked by a single noncompound goal. *Prolog does not have forward chaining.* BTW, Kowalski and I continue to disagree about fundamental nature of pure logic programming. My thesis is that a logic program is characterized by the requirement that each computational step must be completely justified by a rule of mathematical logic.

YeGoblynQueenne 6y ago
Thank you for your reply, professor. Can I ask, what do you mean by "a rule of mathematical logic"? To my mind, resolution should fit the bill, but obviously you're saying something else, since you're critical of resolution. About flattening the structure of a mathematical proposition, I think I understand what you mean, but that should not really be a problem. It should be possible to express a mathematical (or anything) concept in different formalisms without losing its meaning. The structure itself is not that important, as long as the meaning remains the same. Horn logic happens to be a formalism that is both maximally expressive and semi-decidable (SLD-resolution is sound and complete for refutation, or with subsumption). Given that it can also be communicated to a computer without any further changes of formalism, it is also very useful. In any case, thank you again for your contributions to this thread and your replies to my comment. Your perspective of logic programming is invaluable.
- ProfHewitt 6y ago
  You are very welcome! By "a rule of mathematical" logic, I meant a standard logical inference rule such as Modus Ponens or Double Negation Elimination. No modern proof engine requires flattening a proposition into clauses, which often makes the proposition more difficult to understand and process. Just because the clauses are logically equivalent doesn't that they are always useful. Thank you very much for your own contribution :-)
  - YeGoblynQueenne 6y ago
    Ah, so you do mean inference rules? But, resolution is an inference rule so I'm guessing you mean _classical_ logic rules. The way I was taught it (informally) resolution suffices to replace all classic inference rules -but of course there is the restriction of applying it to clauses, which I understand you're not happy with. OK, I think I get it :)
    - ProfHewitt 6y ago
      Good summary :-) A resolution uniform proof procedure had the problem that once all the propositions had been flattened in to clauses, the proof procedure did not have a good idea where to focus its efforts.

YeGoblynQueenne 6y ago

Thank you for your reply, professor. Can I ask, what do you mean by "a rule of mathematical logic"? To my mind, resolution should fit the bill, but obviously you're saying something else, since you're critical of resolution. About flattening the structure of a mathematical proposition, I think I understand what you mean, but that should not really be a problem. It should be possible to express a mathematical (or anything) concept in different formalisms without losing its meaning. The structure itself is not that important, as long as the meaning remains the same. Horn logic happens to be a formalism that is both maximally expressive and semi-decidable (SLD-resolution is sound and complete for refutation, or with subsumption). Given that it can also be communicated to a computer without any further changes of formalism, it is also very useful. In any case, thank you again for your contributions to this thread and your replies to my comment. Your perspective of logic programming is invaluable.

ProfHewitt 6y ago
You are very welcome! By "a rule of mathematical" logic, I meant a standard logical inference rule such as Modus Ponens or Double Negation Elimination. No modern proof engine requires flattening a proposition into clauses, which often makes the proposition more difficult to understand and process. Just because the clauses are logically equivalent doesn't that they are always useful. Thank you very much for your own contribution :-)
- YeGoblynQueenne 6y ago
  Ah, so you do mean inference rules? But, resolution is an inference rule so I'm guessing you mean _classical_ logic rules. The way I was taught it (informally) resolution suffices to replace all classic inference rules -but of course there is the restriction of applying it to clauses, which I understand you're not happy with. OK, I think I get it :)
  - ProfHewitt 6y ago
    Good summary :-) A resolution uniform proof procedure had the problem that once all the propositions had been flattened in to clauses, the proof procedure did not have a good idea where to focus its efforts.