Seeking description of consistency correctness-condition

[Greg Frascadore]

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

[Artur Kornilowicz]

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@...

Dept. of Programming and Formal Methods    http://math.uwb.edu.pl/~arturk/
Institute of Computer Science              tel. [phone]
University of Bialystok                    fax. [phone]
Sosnowa 64, 15-887 Bialystok, Poland

[Greg Frascadore]

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: [e-mail]

Dept. of Programming and Formal Methods    http://math.uwb.edu.pl/~arturk/
Institute of Computer Science              tel. [phone]
University of Bialystok                    fax. [phone]
Sosnowa 64, 15-887 Bialystok, Poland