Sound mathematics is essential in all modern technological developments. As we build increasingly complex systems, mathematical reasoning becomes more difficult and errorprone. Therefore, a computer system is needed that mechanizes the process of doing mathematics. There are two main kinds of mechanized mathematics systems: computer algebra systems that perform many kinds of symbolic computations, and computer theorem proving systems, which support the construction of machine-checked proofs. The objective of this project is to develop a new approach to mechanized mathematics in which computer algebra and computer theorem proving are merged without sacrificing power or soundness. This project completed in March 2003.
Original Research Projects
information technology
-
-
The goal of this project was to apply and enhance the information processing capabilities of neural networks. Applications included finding patterns in large data sets concerning Canadian demographic and consumer buying information, developing pattern recognition and pattern matching networks for use in systems for flood and severe weather forecasting, and developing neural networks for correlating measurements from multiple sensors to assist human operators in making time critical decisions. This project completed in June 2002.
-
Information technology systems such as hardware devices, communication systems and protocols, and software systems are becoming increasingly complex, driven both by advances in technology and by demands for more powerful applications. This project focused on the modelling and verification of reactive systems. The salient characteristics of such systems are those of communication and control, as opposed to computation and data processing. This project completed in June 2002.