Re: Seeking description of consistency correctness-condition
Greg Frascadore <[email protected]>
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <[email protected]> |
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: [email protected] > > 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.