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)
Published Scholars in the Philippines
Using Google Scholar data, webometrics ranks 453 scientists in the Philippines (June 2016 report). Each of these scientists has at least an...
-
Noong unang panahon, sa konstantinopla Hari ang pipino, reyna ang malunggay May anak-anakan na isang prinsesa Bansag na pangalan, si don...
-
119 applicants previously being considered for acceptance by the Harvard Business School (HBS) are now outrightly rejected . These 119 appl...
-
This year has been a roller-coaster ride and I'm glad my wife is always here with me and I with her. We finally have a new home! There...
No comments:
Post a Comment