Sudoku solver

[Marko Rauhamaa]

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>


Marko