Interactive theorem provers: issues faced as a user and tackled as a developer
Interactive theorem provers (ITP for short) are tools whose final aim is to certify proofs written by human beings. To reach that objective they have to fill the gap between the high level language used by humans for communicating and reasoning about mathematics and the lower level language that...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Doctoral Thesis |
| Language: | en |
| Published: |
Alma Mater Studiorum - Università di Bologna
2008
|
| Subjects: | |
| Online Access: | http://amsdottorato.unibo.it/917/ |