On Thu, Mar 26, 2015 at 9:48 AM, Marko Rauhamaa <ma...@pacujo.net> wrote: > Ian Kelly <ian.g.ke...@gmail.com>: > >> On Thu, Mar 26, 2015 at 8:23 AM, Marko Rauhamaa <ma...@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? -- https://mail.python.org/mailman/listinfo/python-list
