ERA

No preview available

Analytics

Share

Permanent link (DOI): https://doi.org/10.7939/R3C84J

Download

Export to: EndNote  |  Zotero  |  Mendeley

Communities

This file is in the following communities:

Computing Science, Department of

Collections

This file is in the following collections:

Technical Reports (Computing Science)

A Note on "How to Write a Proof" Open Access

Descriptions

Author or creator
Rudnicki, Piotr
Trybulec, Andrzej
Additional contributors
Subject/Keyword
proof-checking
proving
automated reasoning
Type of item
Report
Language
English
Place
Time
Description
Technical report TR96-08. We believe that mechanical checking of real-life proofs can become practical and therefore we use Mizar---a proof checking system for proofs written in a style of traditional mathematics. In the beginning of 1994 we came across a copy of L. Lamport's paper in which \"a method for writing proofs is proposed that makes it much harder to prove things that are not true.\" For Mizar users the issue of 'How to Write a Proof?' is an important one, as Mizar is a proof checker and not an automated prover. We have tested Mizar fitness for writing structured proofs in Lamport's style by rewriting his proof of the irrationality of sqrt(2) into Mizar. It was not surprising to notice that formatting conventions help in presenting and reading proofs. However, such conventions do not, as they cannot, guarantee the correctness of the written proof, our little test being a case in point. We advocate development and employment of mechanical checkers for proofs.
Date created
1996
DOI
doi:10.7939/R3C84J
License information
Creative Commons Attribution 3.0 Unported
Rights

Citation for previous publication

Source
Link to related item

File Details

Date Uploaded
Date Modified
2014-04-30T23:03:09.403+00:00
Audit Status
Audits have not yet been run on this file.
Characterization
File format: postscript (Postscript)
Mime type: application/postscript
File size: 188719
Last modified: 2015:10:12 13:33:35-06:00
Filename: TR96-08.ps
Original checksum: 232aa569c0add46798e827792c487850
Activity of users you follow
User Activity Date