Документ взят из кэша поисковой машины. Адрес оригинального документа : http://www.intsys.msu.ru/magazine/archive/v13(1-4)/vtorushin-263-288.pdf Дата изменения: Thu Jul 1 08:45:52 2010 Дата индексирования: Tue Oct 2 00:24:11 2012 Кодировка: IBM-866

. .
, Class Int. , . , .

1.
(). , , . Class Int ([1], [2], [3]). , , , . 1 , , :
& or implies iff


264

. .







.

not true false contradiction thesis ( ) for [st ] (holds ) ex st , {, } (b eing b e)

, , , , . . . , 1 , : м true false contradiction n ot & or implies iff f or h ol d s f o r st h o l d s ex st

& ( )




265

Tm ( ), Tp . ( ), , Tm . Tm ( ), typ e( ) , : 1 , . . . , Tm ( ), , arity( ) = ( 1 , . . . , ), range( ) = typ e( ) , = ( 1 , . . . , ) Tm ( ) typ e( ) = . = . . , , . 1 : &
, &

&

&

&

, ,

. . .




,

м . . . . . . ( )
( )










( ) ( / )


266

. .

=

( / ) ( )

=

( ) ( / ) = , ( ) ( // )

=

, ( )&( ), , . м ( ). . , , , 2 . , 3 . мм . ( ) мм .






мм

мм

, , , . , ( ) . , ( / ) . . = ( // ) , ( ) . , , ( ), , , , . , .




267

- (, PC Mizar [7]). 2 , :
environ text [ ] ; reserve {, } for sort [н> ] func ( ) н> pred [ ] [] ; text [ : ] b egin end [ : ] [by ] {, } pro of qed [ ] ;

text

. .


268

. .

assume thus let [such ] consider [such . .] that {and } = . . .= . . {.= . .}

, () L( 2 ) , . , , . , , , , . (), , , . , , , , , . 1 , 2 , . . . , , ( ) , 1 . ( ) п1 (
1

1

1

п2 (

2

2

(. . . п (

п

+1

)) . . .),

, . , , , ( ) , , .




269

п , -1 ; = &, , , .

, , , м , , п1 (
1 1

п2 (

2

2

(. . . п

-1

(

-1

-1

п )) . . .).

, -, , ; -, , . . . 1) , . 2) typ e( ) . 3) 1 2 (, 1 2 ). , 1 2 , , 2 1 . , - . , , typ e( ) .


270

. .

4) , = 0 1 . . ., , ( ). , , typ e( ) = typ e( ). , , .
environ sort Bo sort Pu pred Ha A: ex W text ok; pil; dRead[Pupil, Book]; being Book st for Y being Pupil holds HadRead[Y,W];

for X being Pupil ex V being Book st HadRead[X,V] proof let X being Pupil; consider W being Book such that B: for Y being Pupil holds HadRead[Y,W] by A; C: HadRead[X,W] by B; thus ex V being Book st HadRead[X,V] by C; qed;

, .
environ sort Book; sort Pupil pred HadRe reserve X, reserve V, A: ex W st

; ad[Pup Y for W for for Y

il, Book]; Pupil; Book; holds HadRead[Y,W];




271

text for X ex V st HadRead[X,V] proof let X; consider W such that B: for Y holds HadRead[Y,W] by A; C: HadRead[X,W] by B; thus ex V st HadRead[X,V] by C; qed;

2.
, . , , , . . , . . , 2 , , , . , . Tp , , , .
, PC Mizar [4].
2


272

. .

1) Tp . , { 1 , 2 } 1 2 . , -, 1 1 2 2 1 2 ; -, 1 2 , 1 2 . 2) (). , Tp . , , 1 2 3 ... : sup . , Tp , Tp . , = { Tp : } , . () Tp ( ) . : Nat , Set н . = { : } . , = { Tp : } . , , ; , 1 2 , 1 . , . , , (, , [4]), , , . , .




273

, , , , , , , , . , . , . Tm , : 1 2 , , , = ( , , vars( ) vars( )), : vars( ) Tm , 1 2 1 ( : typ e( ) = typ e( )). 1 , , = . - , -- . Tm -, -. - . 1 = 2 ( ) , 1 2 . 1 = 2 . , Tm . , , , . , .


274

. .

. , len(cons(Y, rev(L))) len(cons(X, W)) = s(len(W)) s(len(rev(L))). , . , , : 1) , Tm 1 2 . . . 2) , , 2 3 , 1 3 2 , 1 , 2 , 3 Tm .
1

3.

: , , . н . , 1 2 , 3 , 1 3 2 3 . 1 , 2 , 3 Tm . . . 1 2 , : 1 = 2 . , , ; . , , . , , , . .




275

, - . , , , . , 1 , List. , nil() cons(X,L) .
environ sort Nat; func o() -> Nat; func s(Nat) -> Nat; s f f f r 1 2 o u u u e : : rt List; nc nil() -> List; nc cons(Nat, List) -> List; nc conc(List, List) -> List; serve X for Nat, W, U for List; for U holds conc(nil(), U) = U; for X,U,W holds conc(cons(X, U), W) = cons(X, conc(U, W));

func conr(List, Nat) -> List; 3: for X,W holds conr(W, X) = conc(W, cons(X, nil())); func rev(List) -> List; 4: rev(nil()) = nil(); 5: for X,W holds rev(cons(X, W)) = conr(rev(W), X);

, rev(cons(o, cons(s(o), nil))), , List. List: rev(cons(o, conr( conc( conc( cons(s(o), rev(cons(s( rev(cons(s( conr(rev(ni nil o), o), l), ))) nil)), o) nil)), cons(o, nil)) s(o)), cons(o, nil))


276 c c c c c o o o o o n n n n n c c c s s ( ( ( ( ( c c c s s o o o ( ( n n n o o c c s ) ) ( ( ( , , rev( nil, s(o) con con

. .

nil), cons(s(o), nil)), cons(o, nil)) cons(s(o), nil)), cons(o, nil)) , nil), cons(o, nil)) c(nil, cons(o, nil))) s(o, nil)).

:

text rev(cons(o(), cons(s(o()), nil()))) = cons(s(o()), cons(o(), nil())) proof 6: rev(cons(s(o()), nil())) = conr(rev(nil()), s(o())) by 5; 7: conr(rev(nil()), s(o())) = conc(rev(nil()), cons(s(o()), nil())) by 3; 8: conc(nil(), cons(s(o()), nil())) = cons(s(o()), nil()) by 1; 9: conc(nil(), cons(o(), nil())) = cons(o(), nil()) by 1; thus rev(cons(o(), cons(s(o()), nil()))) = conr(rev(cons(s(o()), nil())), o()) by 5 .= conc(rev(cons(s(o()), nil())), cons(o(), nil())) by 3 .= conc(conr(rev(nil()), s(o())), cons(o(), nil())) by 6 .= conc(conc(rev(nil()), cons(s(o()), nil())), cons(o(), nil())) by 7 .= conc(conc(nil(), cons(s(o()), nil())), cons(o(), nil())) by 4 .= conc(cons(s(o()), nil()), cons(o(), nil())) by 8 .= cons(s(o()), conc(nil(), cons(o(), nil()))) by 2 .= cons(s(o()), cons(o(), nil())) by 9; qed;

, , . , List : EmpList, NonEmpList, OrdList .




277

3.
. , - , : 1) , ( , , .); 2) , , () , ; 3) , , ; 4) , , 3 . 5) , . , . , (1646н1716), ( XX ) 1920- . ,
3 . .


278

. .

, , , ( 4 ) . , , ( ) , ( ). ( ) , , 5 . , , . , , . , . , Class Int ([1], [2], [3]). , AProS ([5], [6]), 6 . , .
, (м) , &м . 5 , . 6 AProS . , ( Class Int) .
4




279

, & м( м ). , & ( ( )) . , , . , , . & , ( ) . , , , ( ):
¤ ¤ ¤


¤


¤

( )

, , . & , . , , :
environ pred p[]; pred q[]; 1: p[] & q[]; text not (p[] implies not q[]) proof assume 2: p[] implies not q[];


280
3: p[] by 1; 4: not q[] by 2,3; 5: q[] by 1; thus false by 4,5; qed;

. .

, , . , , , . , . ] [ 1 1, . . . , , , . . . ( [ ] [ ]), , :
environ sort Human; pred drinker[Human]; reserve x, y, t, tt, ttt for Human; text ex x st (drinker[x] implies for y holds drinker[y]) proof assume 1: not ex x st drinker[x] implies for y holds drinker[y]; consider t; 2: drinker[t] implies for y holds drinker[y] proof assume 2: drinker[t];




281

let tt; 3: drinker[tt] proof assume 3: not drinker[tt]; 4: drinker[tt] implies for y holds drinker[y] proof assume 4: drinker[tt]; let ttt; 5: drinker[ttt] proof assume 5: not drinker[ttt]; thus 6: false by 3,4; qed; thus drinker[ttt] by 5; qed; 5: ex x st drinker[x] implies for y holds drinker[y] by 4; thus 6: false by 1,5; qed; thus drinker[tt] by 3; qed; 3: ex x st drinker[x] implies for y holds drinker[y] by 2; thus 4: false by 1,3; qed;

, . , , , . , = 0, ( + )2 = 2 + 2 , :
environ sort Real; func s(Real, Real) -> Real; func o() -> Real; reserve x for Real; 1: for x holds s(x,o()) = x; 2: for x holds s(o(),x) = x; sort Vector; func f(Vector, Vector) -> Vector;


282

. .

func h(Vector, Vector) -> Real; reserve u,v,w for Vector; 3: for u,v,w holds h(f(u,v),w) = s(h(u,w),h(v,w)); 4: for u,v,w holds h(u,f(v,w)) = s(h(u,v),h(u,w)); text for a, b being Vector st h(a,b) = o() & h(b,a) = o() holds h(f(a,b),f(a,b)) = s(h(a,a),h(b,b)) proof let a be Vector,b be Vector; assume 5: h(a,b) = o() & h(b,a) = o(); 6: h(f(a,b),f(a,b)) = s(h(a,f(a,b)),h(b,f(a,b))) by 3; 7: h(a,f(a,b)) = s(h(a,a),h(a,b)) by 4; 8: h(a,b) = o() by 5; 9: s(h(a,a),o()) = h(a,a) by 1; 10: h(b,f(a,b)) = s(h(b,a),h(b,b)) by 4; 11: h(b,a) = o() by 5; 12: s(o(),h(b,b)) = h(b,b) by 2; thus h(f(a,b),f(a,b)) = s(h(a,f(a,b)),h(b,f(a,b))) by 6 .= s(s(h(a,a),h(a,b)),h(b,f(a,b))) by 7 .= s(s(h(a,a),o()),h(b,f(a,b))) by 8 .= s(h(a,a),h(b,f(a,b))) by 9 .= s(h(a,a),s(h(b,a),h(b,b))) by 10 .= s(h(a,a),s(o(),h(b,b))) by 11 .= s(h(a,a),h(b,b)) by 12; qed;

4.
(, ) 1 . , . , , , . , , ; , , , . .




283

(, ) := () (assume ) (, ) (thus ) = (, ) -2(, )

(, ) . . . . .
(, ) ( imp ) ( & ) holds ) (for 1 , . . . , 1 . . . . 2 ... . . (ex 1 , . . . , st ) = lvar() 1 , . . . , type( 1 ), . . . , type( ) ), 1 1( 1, . . . , 2 ( 1 , . . . , ), 2 ... ( 1, . . . , ) lvar() ( = 1, . . . , )

type( type( type(

1 2

), ), )



,


284

. .

- , . , , . , . , . .
() (for holds ) type( ) (let ) := [ ] ( imp ) (assume ) := ( & ) (thus ) := (thus )

, . , . = : 1) 1 = 2 1 2 , . 2) , , . 3) , , .




285

4) , , . 5) , . , , . , , , . , , . .
(, ) := :: (true) ( = ) := { } :: := ( 1 = 2 ) ( 1 , 2 , ) := { } := := := :=

( & ) ((, ), (, )) ( or ) {(, ), (, )} (ex st ) {(, [ . . type( )])} (for holds ) ( imp ) {(, )}

( ( 1 = 2 ) ( or ) (false)) :: := , (, , )


286

. .

:= {(, := := {-(, )}

, ) }

- .
-(, ) :: := := , ( imp ) (, , ) := {(-( , ), )} := := :: := , (1 or 2 ) . 1 , 2 , (1 , 1 , ) (2 , 2 , ) . 1 , 2 , 1 , 2 , (1 imp 1 , 1 ) (2 imp 2 , 2 ) := -( , ) , ) 1 := ( , := (1 imp 1 , 1 , ) 2 3 := (2 imp 2 , 2 , ) := (( 2 , 3 ), 1 ) :=

-2 .




287

-2(, ) := , -( , ) ( or ) 1 := (, imp ) 2 := (, imp ) , ) 3 := ( or , := (( 1 , 2 , ), 3 )

- . .
-( , ) := ( , ) {
1

2 ...

, . . , .

1

} = lvar() . . type( . . type(
. . type(

1 2

), ), )

. , . . , , , , 0. ( ), ( ) , . , 1 , . , ( ) , ( ).


288

. .


[1] . ., . ., . . CLASS INT // - 2006 I I I - - 2006 , : - , 2006. [2] . ., . ., . . CLASS INT // - - 2007 IV - - 2007 , : - , 2007. . 174н176. [3] . ., . ., . . CLASS INT // - - 2008 V - - 2008 , : - , 2008. [4] Bancerek G. On the structure of Mizar typ es // Electronic Notes in Theoretical Computer Science. 85. 2003. P. 69н85. [5] Sieg W., Byrnes J. Normal natural deduction pro of (in classical logic) // Studia Logica. 60 (1). 1998. P. 67н106. [6] Sieg W., Cittadini S. Normal natural deduction pro of (in non-classical logic) // Mechanizing Mathematical Resoning. LNAI 2605. 2005. P. 169н191. [7] Trybulec A., Wiedijk F. CHECKER notes on the basic inference step in Mizar. 2000 / available at http://www.cs.kun.nl/~freek/mizar/by.dvi.