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> Marko -- https://mail.python.org/mailman/listinfo/python-list
