Gradual computerisation and verification of mathematics : MathLang's path into Mizar
There are many proof checking tools that allow capturing mathematical knowledge into formal representation. Those proof systems allow further automatic verifica- tion of the logical correctness of the captured knowledge. However, the process of encoding common mathematical documents in a chosen proo...
| Main Author: | |
|---|---|
| Other Authors: | |
| Published: |
Heriot-Watt University
2009
|
| Subjects: | |
| Online Access: | http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.507912 |