[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] referring to unlabeled theorems
On Sat, 17 Feb 2007, Jesse Alama wrote:
Adam Naumowicz <adamn@math.uwb.edu.pl> writes:
On Sat, 17 Feb 2007, Jesse Alama wrote:
One thing that annoys me slightly is that the .miz form of a MIZAR
article doesn't necessarily have labels for all theorems. I prefer to
look at MIZAR articles (not abstracts) in emacs, and sometimes I find
an unlabeled theorem that I want to use. In these situations I have
to look at, e.g., the semantic presentation of that article or the
abstract to find out how to refer to that theorem. It would be nice
if theorems in .miz files were labeled as they are in the abstracts
and the semantic presentation.
It's because all articles are as a rule cleansed of all unnecessary
labels, i.e statements not referred to in the current article
shouldn't be labelled. Theorems are no exception here.
When I was studying GOEDELCP a while ago, I was surprised to see that
the final theorem of the article, (a version of) the completeness
theorem for first-order logic, didn't get a label. But (I thought
then) what if I want to work on, say, a proof of compactness for
first-order logic? How would I refer to the completeness theorem? As
a beginner to the world of MIZAR, I found it baffling that theorems
and lemmas needed to prove the completeness theorem are given labels,
but that the completeness theorem itself was unlabeled. If anything
deserves a label in that file, it's that theorem!
You're absolutely right, but the vast majority of users treat the *.miz
files as "raw data", and prefer to browse/search the abstracts instead -
this is what the abstracts were devised for ;-) The *.miz files are
good for more thorough studies of proofs, though.
It would be great if the .miz files were not cleaned up as you say
they are; adding the labels would be, in my opinion, a small
improvement to the (.miz file) presentation of the MML.
It's not a big deal to put the labels there, but I think the Library
Committee would have to change some utilities they now use, e.g. for
automatic removal of unnecessary items and the like. The library is rather
frequently processed with quite a few automatic scripts that may depend on
this...
Best,
Adam Naumowicz
======================================================================
Department of Applied Logic fax. +48 (85) 745-7662
Institute of Computer Science tel. +48 (85) 745-7559 (office)
University of Bialystok e-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland http://math.uwb.edu.pl/~adamn/
======================================================================