Sudoku solver

[Marko Rauhamaa]

Ian Kelly <ian.g.kelly at gmail.com>:

> On Thu, Mar 26, 2015 at 9:48 AM, Marko Rauhamaa <marko at pacujo.net> wrote:
>> 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?

Trial-and-error was presented in opposition to logical deduction, while
really trial-and-error *is* logical deduction.


Marko