[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] Seeking description of consistency correctness-condition
Artur,
Thanks! That is _exactly_ what I was seeking.
I had seen the lecture notes at
http://markun.cs.shinshu-u.ac.jp/kiso/projects/proofchecker/mizar/Mizar4/index-e.html
but the page you cited for me (below) is not mentioned in those notes (or
anywhere else according to google links).
-Greg Frascadore
Artur Kornilowicz wrote:
>
> Hello,
>
> please look at
>
> http://markun.cs.shinshu-u.ac.jp/kiso/projects/proofchecker/mizar/skeletons/toc.html
>
> In Section '3. Definitions' you can find an answer.
>
> Best,
>
> Artur
>
>
>
> On Fri, 23 Oct 2009, Greg Frascadore wrote:
>
>>
>> Hello,
>>
>> I'm looking for a description of the 'consistency' correctness-
>> condition and the situations where it is required. Particularly, a
>> statement of the template formula one must prove to establish
>> consistency.
>>
>> After looking through some old papers like 'Muzalewski1993 PCMizar',
>> and Matuszewski+Rudnicki 'Mizar: the first 30 years', I either couldn't
>> find it, or only a brief mention that it is required for 'definitions
>> per cases'.
>>
>> Searching the MML, consistency is usually demonstrated simply as:
>> consistency; (due to disjointness of if/otherwise ?)
>>
>> But in the non-trivial cases, the condition being proved isn't
>> obvious to me.
>>
>> Thanks,
>>
>> -Greg Frascadore
>>
>> --
>> View this message in context:
>> http://www.nabble.com/Seeking-description-of-consistency-correctness-condition-tp26027415p26027415.html
>> Sent from the Mizar mailing list archive at Nabble.com.
>>
>>
>
>
> ==========================================================================
>
> Artur Kornilowicz e-mail: arturk@math.uwb.edu.pl
>
> Dept. of Programming and Formal Methods http://math.uwb.edu.pl/~arturk/
> Institute of Computer Science tel. +48 (85) 745-7662
> University of Bialystok fax. +48 (85) 745-7662
> Sosnowa 64, 15-887 Bialystok, Poland
>
>
--
View this message in context: http://www.nabble.com/Seeking-description-of-consistency-correctness-condition-tp26027415p26035165.html
Sent from the Mizar mailing list archive at Nabble.com.