Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!cornell!oravax!harper
From: harper@oravax.UUCP (Douglas Harper)
Newsgroups: comp.theory
Subject: Proof theory (was Re: Academic legend)
Message-ID: <1318@oravax.UUCP>
Date: 5 Feb 90 16:46:49 GMT
References: <20433@watdragon.waterloo.edu> <2072@rex.cs.tulane.edu> <19983@netnews.upenn.edu>
Organization: Odyssey Research Associates, Ithaca NY
Lines: 23
Summary: Proof theory is alive, well and prospering

In article <19983@netnews.upenn.edu>, aaron@grad2.cis.upenn.edu (Aaron Watters) writes:
| In article <2072@rex.cs.tulane.edu> fs@rex.UUCP (Frank Silbermann) writes:
| >A notation is but a language, and a proof theory
| >merely a way of verifying one's hypotheses.
| >The models are what make a theory interesting.
| 
| I like the spirit, but I have to object that `proof theories' are
| seldom used at all (except for trivial things like type checking
| and getting students to drop your class on symbolic logic).  Proof
| theories are primarily an abstract object of mathematical discussion
| and not a used mathematical technique.
|   -aaron

Mr. Watters is apparently unaware of the widespread use of proof theory
in pure and applied logic.  Two applications that readers of this
newsgroup will immediately recognize are automated theorem proving and
program verification.

-- 
Douglas Harper                     oravax!harper@cu-arpa.cs.cornell.edu
"Gimme eat."..."Give *everybody* eat!"
	-- Major _____ de Coverley
		-- Joseph Heller, _CATCH-22_