Tata Institute of Fundamental Research
Formal Proofs: From Principia Mathematica to Automated Reasoning
Colloquium
Speaker:
N. Raja
School of Technology and Computer Science
Tata Institute of Fundamental Research
Homi Bhabha Road
Mum
Date:
Wednesday, 8 Dec 2010 (all day)
Venue:
A-212 (STCS Seminar Room)
(Scan to add to calendar)
Abstract:
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.
| Speaker: | N. Raja School of Technology and Computer Science Tata Institute of Fundamental Research Homi Bhabha Road Mum |
| Date: | Wednesday, 8 Dec 2010 (all day) |
| Venue: | A-212 (STCS Seminar Room) |
(Scan to add to calendar)
Abstract:
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.