Re: [mizar] Seeking description of consistency correctness-condition

[Artur Kornilowicz <arturk@math.uwb.edu.pl>]

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