| Description |
The year 2010 is the centenary of Whitehead and Russell's `Principia Mathematica'. With the advent of computer science the notion of formal proofs from `Principia' have evolved from a mere theoretical curiosity to something that is possible in practice. Recent advances in the field of `Interactive Proof Checking' with the associated development of powerful tools such as `Proof Assistants' have given rise to an interesting consequence -- viz. the practical feasibility of importing techniques developed in the computer science community and redeploying them to improve the main activity of the working mathematician, namely the process of proof development. At the core of such redeployed techniques lie the notions of formal systems, formal reasoning, and formal proofs. However the process of formalizing mathematics is a highly non-trivial task, and gives rise to a number of challenging and interesting issues. This talk will give an overview of related research in the area of automated reasoning.
|