RW wrote:I don't think that anyone is saying that patterns should not be used. Patterns have many advantages over proposition chains
So, that's it.
You're not speaking of the same thing as me.
I never spoke of proposition chains (with all the stuff of weak and strong links).
My chains are not chains of inferences. They are patterns of well defined type and length.
With each chain type is associated a chain rule (which is a mathematical theorem) that allows some predefined eliminations in some predefined cells. You are not supposed to re-prove the chain rule each time you're using it.
The notions of weak links, strong links and chains of inferences are at the origin of a total confusion between chain patterns and chains of reasoning.
But, when you have found an xy-chain, this allows some eliminations, as a Hidden-Pairs would, and this supposes absolutely no hypothesis. You're just applying a theorem.
RW wrote:I don't see why a solver should be limited to a set of predefined rules.
Who said the set of rules should be limited? You can always devise new resolution rules.
RW wrote:Here's what I disagree with the most:
denis_berthier wrote:One of the reasons for my introducing the notion of a resolution rule is that with them we are sure we are not using disguised forms of T&E. I consider that they are the proper formalisation for a "pure logic solution".
With this you clearly say that solving by the defined rules is "pure logic" while any other technique is not as it could be "disguised T&E". I wouldn't condemn the use of T&E like that, because it is as logical as any other technique. The rules of sudoku are very simple, I don't see the need for additional rules that restrict what techniques may or may not be used.
The fact is most people don't accept T&E in a solution.
RW wrote:T&E also helps you understand the logic behind any pattern based elimination. We see people all the time here who have read about a pattern, but not understood the basic logic that allows the elimination, then they use the pattern in the wrong way. All that is required is to understand that if a pattern allows you to eliminate a candidate, it is because if the candidate was true, then there would be a contradiction in the pattern cells. This very simple rule explains all pattern based elimintaions, yet I hardly ever see it in a technique explanation because the word "if" is considered too T&E...
I can't see any relation between using "if" while you are proving a theorem and using T&E while you are solving a puzzle. These are two different activities.
But you're still thinking that you must re-prove a chain rule every time. Why then not re-prove also the rules for fish?
The origin of this confusion is the same as I indicated above.
RW wrote:denis_berthier wrote:I don't know what a nested chain is.
Well, mostly when solvers have exhausted the possibilities using chains with singles, the next step is chains with locked candidates, followed by chains with subsets and so on. When the concept of "chain" is expanded enough in this way, we sooner or later arrive at "chains with chains" which solve all puzzles, just like T&E does.
As far as I know even these extended chains cannot solve Easter Monster.
Anyway, in my chains, there are neither ALS nor subsets of any kind and they solve "only" 99,99% of the minimal puzzles.