Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Posting-Version: version B 2.10.1 6/24/83; site druky.UUCP
Path: utzoo!watmath!clyde!burl!ulysses!mhuxr!mhuxt!houxm!mtuxo!drutx!druky!krahl
From: krahl@druky.UUCP (KrahlRH)
Newsgroups: net.singles
Subject: Re: Re: Responsibility and blame (math question)
Message-ID: <944@druky.UUCP>
Date: Thu, 1-Aug-85 12:21:30 EDT
Article-I.D.: druky.944
Posted: Thu Aug  1 12:21:30 1985
Date-Received: Sat, 3-Aug-85 01:44:10 EDT
References: <547@wdl1.UUCP>
Organization: AT&T Information Systems Laboratories, Denver
Lines: 17

>      The ``obvious proof'' chestnut surfaces again.  ``Obvious'' means that
>you can find the proof without extensive search; i.e. exploration of blind
>alleys and backtracking is minimal.  Obvious proofs may be long, but the work
>all moves the proof forward.  Those of us who have worked in automatic theorem
>proving are very aware of the difference between an obvious proof and an
>short but non-obvious proof; theorem provers are good at obvious proofs.
>      Let's quit discussing mathematics in net.singles.
>
>					John Nagle


	Good *idea* John,....LET'S !!

-- 
				       Rich Krahl  ..!drutx!druky!krahl

"You can't get what you want..'til you know what you want" -Joe Jackson