Sudoku solver

[Ian Kelly]

On Thu, Mar 26, 2015 at 9:48 AM, Marko Rauhamaa <marko at pacujo.net> wrote:
> Ian Kelly <ian.g.kelly at gmail.com>:
>
>> On Thu, Mar 26, 2015 at 8:23 AM, Marko Rauhamaa <marko at pacujo.net> wrote:
>>> That's trial and error, aka, reductio ad absurdum.
>>
>> Okay, I've probably used single-lookahead trial and error in my
>> reasoning at some point. But the example you give is equivalent to the
>> deductive process "That can't be a 5, so I remove it as a candidate.
>> The only place left for a 5 is here, so I remove the 2 as a candidate
>> and fill in the 5."
>
> In fact, the "trial-and-error" technique is used in automated theorem
> proving:
>
>   Lean provers are generally implemented in Prolog, and make proficient
>   use of the backtracking engine and logic variables of that language.
>
>   <URL: http://en.wikipedia.org/wiki/Lean_theorem_prover>

Sure, but what has this to do with the statement that *sudoku* should
not require trial and error to solve?