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)
-
Noong unang panahon, sa konstantinopla Hari ang pipino, reyna ang malunggay May anak-anakan na isang prinsesa Bansag na pangalan, si don...
-
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...
-
Tar heels came very close to upset the Hokies today -- missing 3 points due to missed 54 yard field goal to tie the game in the 4th quarter....
No comments:
Post a Comment