Path: csiph.com!usenet.pasdenom.info!news.redatomik.org!newsfeed.xs4all.nl!newsfeed2.news.xs4all.nl!xs4all!post.news.xs4all.nl!not-for-mail
MIME-Version: 1.0
In-Reply-To: <87vbhnn4jt.fsf@elektro.pacujo.net>
References: <87r3sdnw5t.fsf@elektro.pacujo.net> <mailman.188.1427358005.10327.python-list@python.org> <87fv8sndw1.fsf@elektro.pacujo.net> <mailman.197.1427375759.10327.python-list@python.org> <874mp7on13.fsf@elektro.pacujo.net> <mailman.205.1427382450.10327.python-list@python.org> <87vbhnn4jt.fsf@elektro.pacujo.net>
From: Ian Kelly <ian.g.kelly@gmail.com>
Date: Thu, 26 Mar 2015 10:20:10 -0600
Subject: Re: Sudoku solver
To: Python <python-list@python.org>
Content-Type: text/plain; charset=UTF-8
Precedence: list
Newsgroups: comp.lang.python
Message-ID: <mailman.209.1427386861.10327.python-list@python.org>
Lines: 22
NNTP-Posting-Host: 2001:888:2000:d::a6
Xref: csiph.com comp.lang.python:88074

On Thu, Mar 26, 2015 at 9:48 AM, Marko Rauhamaa <marko@pacujo.net> wrote:
> Ian Kelly <ian.g.kelly@gmail.com>:
>
>> On Thu, Mar 26, 2015 at 8:23 AM, Marko Rauhamaa <marko@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?