Tuesday, April 05, 2005

The QED Manifesto

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. :)
at

No comments:

Post a Comment

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...

  • First day of work
    Written a program to generate a couple of reports, prepared a description of statistical analysis of ozone stress data, studied possible sta...
  • Popped!
    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...
  • Self powering robot
    Talk about scifi becoming real -- a team of scientists and engineers at University of the West of England (U.W.E.) developed a robot that dr...