harper@oravax.UUCP (Douglas Harper) (02/06/90)
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_
aaron@grad2.cis.upenn.edu (Aaron Watters) (02/06/90)
In article <1318@oravax.UUCP> harper@oravax.UUCP (Douglas Harper) writes: >In article <19983@netnews.upenn.edu>, aaron@grad2.cis.upenn.edu (Aaron Watters) writes: >| 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. I geuss I am. I know these people STUDY proof theories -- that's not the same as using it. By `use' I did not mean `prove things about.' >Two applications that readers of this >newsgroup will immediately recognize are automated theorem proving and >program verification. I said `seldom' not `never.' These uses are hardly widespread -- especially not by real mathematicians. --aaron PS: Still waiting for the formal spec and verification of the triangle program.-a.
harper@oravax.UUCP (Douglas Harper) (02/06/90)
In article <20010@netnews.upenn.edu>, aaron@grad2.cis.upenn.edu (Aaron Watters) writes: [Several things with which I disagree.] I have sent him email rather than publicly continue a discussion which doesn't seem to generate much interest within the readership of this newsgroup. If future postings show me wrong, I'll rejoin the public discussion. > PS: Still waiting for the formal spec and verification of the > triangle program.-a. He will have it, but it will take some time to build the theory up from the axioms. The verification in terms of a specification governed by that theory is already completed. I intend to post the final version in sci.logic. If enough people request it in the meantime, I'll cross-post it here when it's done. -- Douglas Harper oravax!harper@cu-arpa.cs.cornell.edu "Gimme eat."..."Give *everybody* eat!" -- Major _____ de Coverley -- Joseph Heller, _CATCH-22_
ian@oravax.UUCP (Ian Sutherland) (02/06/90)
In article <1319@oravax.UUCP> harper@oravax.UUCP (Douglas Harper) writes: -In article <20010@netnews.upenn.edu>, aaron@grad2.cis.upenn.edu (Aaron Watters) writes: -- PS: Still waiting for the formal spec and verification of the -- triangle program.-a. - -He will have it, but it will take some time to build the theory up from -the axioms. The verification in terms of a specification governed by -that theory is already completed. I intend to post the final version -in sci.logic. If enough people request it in the meantime, I'll -cross-post it here when it's done. I request that you ONLY post it in comp.theory. It seems to me that proofs of correctness of programs are not really that interesting from the point of view of mathematical logic. -- Ian Sutherland ian%oravax.uucp@cu-arpa.cs.cornell.edu Sans Peur
yodaiken@freal.cs.umass.edu (victor yodaiken) (02/12/90)
In article <20010@netnews.upenn.edu> aaron@grad2.cis.upenn.edu.UUCP (Aaron Watters) writes: >>Mr. Watters is apparently unaware of the widespread use of proof theory >>in pure and applied logic. >I geuss I am. I know these people STUDY proof theories -- that's not >the same as using it. By `use' I did not mean `prove things about.' > >I said `seldom' not `never.' These uses are hardly widespread >-- especially not by real mathematicians. > --aaron > Look at "Bounded Arithmetic" by Sam Buss (Bibliopolis 1986) for an iteresting"real mathematic" use of proof theory.
aaron@grad2.cis.upenn.edu (Aaron Watters) (02/13/90)
In article <9993@dime.cs.umass.edu> yodaiken@freal.cs.umass.edu (victor yodaiken) writes: >In article <20010@netnews.upenn.edu> aaron@grad2.cis.upenn.edu.UUCP (Aaron Watters) writes: >Look at "Bounded Arithmetic" by Sam Buss (Bibliopolis 1986) >for an iteresting"real mathematic" use of proof theory. I apologise for using bad terminology. I suppose the proof of the semidecidability of first order predicate calculus could be called a `use' of proof theory -- and it's certainly good mathematics. This is not the sense I meant when I said that proof theory was seldom `used' by mathematicians. I meant `use' in the sense of `no sensible programmer uses turing machines.' I.e, turing machines are a theoretical object of study and not a practical way to implement programs. I should have said that the original posting was misleading because it suggested that mathematicians operate within the realm of formal proofs, which they don't. Proof theories are a theoretical object of study and not a practical way to arrive and mathematical truth. -aaron.