کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
421583 | 684904 | 2012 | 16 صفحه PDF | دانلود رایگان |
For interactive theorem provers a very desirable property is consistency: it should not be possible to prove false theorems. However, this is not enough: it also should not be possible to think that a theorem that actually is false has been proved. More precisely: the user should be able to know what it is that the interactive theorem prover is proving.To make these issues concrete we introduce the notion of Pollack-consistency. This property is related to a system being able to correctly parse formulas that it printed itself. In current systems it happens regularly that this fails.We argue that a good interactive theorem prover should be Pollack-consistent. We show with examples that many interactive theorem provers currently are not Pollack-consistent. Finally we describe a simple approach for making a system Pollack-consistent, which only consists of a small modification to the printing code of the system.
Journal: Electronic Notes in Theoretical Computer Science - Volume 285, 19 September 2012, Pages 85-100