The scope of automated deduction is not limited to the traditional areas of computer science and mathematics. In response to our call for contributions on future directions, Michael Musuch, Jaap Kamp, and others at the University of Amsterdam highlighted one of the most important long-term roles of automated deduction: the use of AD in building and testing theories. Musuch and colleagues are investigating the use of AD techniques in building formal theories in the social sciences [88] [89]. These formal theories allow the testing of hypotheses for consistency and logical consequence. The ability to determine the logical consequences of a formally specified theory not only saves expensive field studies but yields a more precise representation of the current hypotheses of the field. Alternative theories are more easily assessed, as well. This opportunity to use formal methods to advance and test various theories highlights the need for more axiomizations of subdisciplines and problem areas.
Looking to the more distant future, we see that the use of formal methods to study major disciplines may be the most significant intellectual application of AD technology, for it can encompass most of human intellectual endeavors. Our field has undertaken to build general reasoning engines that make the idea of formal theories of knowledge useful. Within the realm of mathematics we have put forth proposals to verify, classify, and archive the main results of the various branches of the subject. The QED project, now in the formative stage, has the audacious goal of building a computer system to effectively represent all important mathematical knowledge and techniques [91]. Important questions arise immediately, such as the question of presentation of the mathematical theorems and theories. Should we strive to have theorems verified within a fixed framework? Is it acceptable to have multiple systems certified for verification of theorems? Phrasing this at a more fundamental level, do we choose a constructivist mathematics as our framework (perhaps a bias of computer science-oriented mathematicians) or a classical foundation? This is clearly a long-range project, but one where success adds a new dimension to the world of mathematics. More correctly, it would extend the ambitions of the Bourbaki group [13] (to formalize mathematics) to a level of rigor only dreamed about when the Bourbaki effort began.
Another project, the Mizar project, originally undertaken by Polish mathematicians to provide software support for writing mathematics papers, has developed into an attempt to formalize large portions of mathematics. Thus many regard this project as an interesting start toward the QED concept. The Mizar project is well under way, even maintaining its own electronic journal, the Journal of Formalized Mathematics. Although some technical material appears in hard copy, the project is truly oriented to effectively use the capabilities of the electronic medium, including extensive cross-referencing practical only in an electronic environment. For more information the reader should consult the Web site http://web.cs.ualberta.ca:80/piotr/Mizar/. What now exists is a substantial number of formal proofs, proof checked by machine based on a fixed axiom set. The effort now has some foreign (to Poland) sites active in the effort. Much has been accomplished with little funding, and some people in the automated deduction community feel strongly that this project should receive more financial support from the international community. (We understand that the Journal of Formalized Mathematics does receive funding from the Office of Naval Research.) These attempts to formalize the core of mathematics will certainly be paralleled by projects in engineering, medicine, law (underway at present), and the social sciences. For those who dismiss this projection with the comment that all such models (except mathematics and law) should be stochastic, we remind them that no probabilistic inference theory yet exists that is practical for large formal systems. It may be true that traditional formal theories can be viewed only as approximations for the real world in most settings, but, as Musuch's note is telling us, they are still of great importance when complex domains are under study.