Xref: utzoo sci.math:11630 sci.logic:872 comp.theory:828
Path: utzoo!attcan!uunet!cs.utexas.edu!rutgers!netnews.upenn.edu!grad2.cis.upenn.edu!aaron
From: aaron@grad2.cis.upenn.edu (Aaron Watters)
Newsgroups: sci.math,sci.logic,comp.theory
Subject: Re: Question about the Four Color Proof
Message-ID: <26843@netnews.upenn.edu>
Date: 9 Jul 90 13:35:12 GMT
References: <9578@hubcap.clemson.edu>
Sender: news@netnews.upenn.edu
Reply-To: aaron@grad2.cis.upenn.edu.UUCP (Aaron Watters)
Organization: University of Pennsylvania
Lines: 11

Just a comment.

The four color proof is often mistakenly cited as a triumphant
example of the use of formal methods -- most egregiously in a
paper about program derivation by Scherlis and Scott.

Just thought I'd point out that the proof is in no sense any
more formal than most other proofs you'll find out there,
even though it includes an algorithm as part of the proof,
together with a claim that the algorithm terminated with
a given result.		-aaron