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