[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] Re: what's new in mizar?
On Fri, 14 Dec 2007, Jesse Alama wrote:
Excellent! I'm glad to hear that the checker can now handle a wider
class of "obvious" inferences. Are there cases in the MML where this
really arises? In other words, if, say, trivdemo is run on the old MML,
do we find any cases where the text could be simplified?
Indeed, there were quite a few such cases where 'trivdemo' detected proofs
that could be simplified to a straightforward justification (see.
RELAT_1:9 for example). But adjusting the library according to what
'relinfer' reports is even more important.
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/
======================================================================