Hammering towards QED
This paper surveys the emerging methods to automate reasoning over large libraries developed with formal proof assistants. We call these methods hammers. They give the authors of formal proofs a strong "one-stroke" tool for discharging difficult lemmas without the need for careful and deta...
| Những tác giả chính: | , , , |
|---|---|
| Định dạng: | Bài viết |
| Ngôn ngữ: | English |
| Được phát hành: |
University of Bologna
2016-01-01
|
| Loạt: | Journal of Formalized Reasoning |
| Những chủ đề: | |
| Truy cập trực tuyến: | http://jfr.unibo.it/article/view/4593 |