Automatic Proof Checking and Proof Construction by Tactics
Overview & Synopsis
In this note we compare two kinds of systems that verify the correctness of mathematical developments: proof checking and proof construction by tactics and we propose to merge them in a single system. We consider mathematics formalized in the Calculus of Constructions [3] [4] but the ideas given here are not specific to this formalism. As an example of a proof checking system we consider the constructive engine of the system Coq [11] and as an example of a proof construction by tactics system we consider the proof assistant of the system Coq [7] designed in the spirit of the system LCF [8]
Indexed from repository: HAL Open Science
(
hal.science)
Keyboard Shortcuts:
← / → for pages • + / - for zoom • 0 to fit width
Powered by Mozilla PDF.js v3.11
Document Information
| Document Title | Automatic Proof Checking and Proof Construction by Tactics |
|---|---|
| Author / Organization | Gilles Dowek |
| Subject & Discipline | Multidisciplinary Academic Open Research |
| Categories | Science & Mathematics |
| Publication Year | 1991 |
| License / Rights | Open Access / Creative Commons |
| Resource Verification | Listed PDF (Verification Pending) |
| Original Host Website |
HAL Open Science
(hal.science)
|
| File Format | application/pdf (Portable Document Format) |
| Language | EN |
| Catalog ID | DOC-240476 |
| Original Source Link | Visit Source Page on hal.science » |