2 ms·
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.
by 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 agoAh, 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 agoGood 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.