QUOD erat demonstrandum (QED): meaning "which was to be shown" has been used to end a formal proof of a mathematical proposition. Some mathematicians use a black square instead of QED. In UP, there's a professor (I forgot his name), who uses T.N. instead. T.N. means "tapos na". :)
The QED manifesto describes a project that aims to automate doing formal proofs using a computer. The four-color problem is the most famous theorem proved using a computer generated proof. I'm not quite sure how feasible this project is -- proving that a program has no bugs is in fact difficult.
Now, how can you prove that a computer program P which proves a theorem to be true has no bugs? Write another program Q that proves P has no bugs? I'm now confused. :)
Subscribe to:
Post Comments (Atom)
-
So much for the bubble -- the hokies are about to burst theirs. The yellow jackets are currently pulling away from the hokies. The tigers ho...
-
Written a program to generate a couple of reports, prepared a description of statistical analysis of ozone stress data, studied possible sta...
-
I thought the wolfpack would get a touchdown its last drive during the dying minutes of the 4th quarter. However, they came short and the ho...
No comments:
Post a Comment