![]()
| ||
(Jon sez:) ![]() Our goal is to develop techniques and build practical programs to help mathematicians, logicians, scientists, engineers, and others with some of the deductive aspects of their work. Most of our work applies to problems that can be stated in the language of first-order logic with equality. Our programs have been applied to many real problems, mostly in abstract algebra and logic, and many new results have been obtained through their use.Automated reasoning has made real contributions to science and mathematics, such as the 1997 proof of the Robbins Conjecture. The current crop of automated reasoning programs need a lot of tending by knowledgable humans. If we can get computers working, by themselves, on advancing science and mathematics, we'll be partway to the Singularity as Vinge imagines it. Patch such a system into a hardware-sharing setup like SETI@home, and the sky would be the limit. The Internet is such a wonderful place that if you want to play with automated reasoning, you can do so at Son of Birdbrain. |
(Mark sez:) ![]() There's always more Mars news. While Spirit and Opportunity, having completed their primary objectives (searching out evidence of water on Mars in the past) have had their missions extended to September, NASA is already looking ahead to the next class of rovers: the Mars Science Laboratory, a six-wheeled, automobile-sized behemoth that will have the power and endurance to carry out a mission lasting years. MSL will be able to travel large enough distances that it could visit interesting terrain features (such as the Mariner Valley) which are too hazardous to be directly landed on. And let's not neglect the fact that this "skycrane" thing they want to use to set it down on the surface is just darned cool. |