Formal methods are successfully used in a wide range of applications - from hardware and software verification to formalizing mathematics and education. This talk with provide an overview of several most commonly used approaches to computer-aided formal reasoning. We will also show how these approaches could be efficiently combined in a single "generic" theorem proving system. Such generic system could serve as a common platform for bringing together and combining the advantages of specialized tools. It can also be used as a toolkit for trying out new approaches to computer-aided formal reasoning and for quick development of new formal tools.

Alexei Nogin got Ph.D. in Computer Science from Cornell University. He is now a coordinator of MetaPRL Proof Assistant and Logical Programming Environment project http://cvs.metaprl.org:12000/metaprl/