We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
Proof assistants: History, ideas and future.
- Authors
Guevers, H.
- Abstract
In this paper I will discuss the fundamental ideas behind proof assistants: What are they and what is a proof anyway? I give a short history of the main ideas, emphasizing the way they ensure the correctness of the mathematics formalized. I will also briefly discuss the places where proof assistants are used and how we envision their extended use in the future. While being an introduction into the world of proof assistants and the main issues behind them, this paper is also a position paper that pushes the further use of proof assistants. We believe that these systems will become the future of mathematics, where definitions, statements, computations and proofs are all available in a computerized form. An important application is and will be in computer supported modelling and verification of systems. But there is still a long road ahead and I will indicate what we believe is needed for the further proliferation of proof assistants.
- Subjects
PROOF theory; CONFIRMATION (Logic); LOGIC; MATHEMATICS; MODELING (Sculpture)
- Publication
Sādhanā: Academy Proceedings in Engineering Sciences, 2009, Vol 34, Issue 1, p3
- ISSN
0256-2499
- Publication type
Article