Postano: 14:16 pon, 31. 3. 2014| Formally Verified Mathematics (napisa): |
| Due to developments in computer science over the past few decades, it is now possible to achieve complete formalization in practice. Working with "computational proof assistants," users are able to verify substantial mathematical theorems, constructing formal axiomatic derivations of remarkable complexity. Our goal in this article is to describe the current technology and its motivations, survey the state of the art, highlight some recent advances, and discuss prospects for the future. |
output generated using printer-friendly topic mod. Vremenska zona: GMT + 01:00.