50 Recent Changes in Mizar Web retrieved at 03:56 (GMT)
Mizar syntax GrzegorzBancerek 13 Jun 2009 Adjective with arguments, no predicative synonyms/antonyms for adjective formulae, canceled registrations. GrzegorzBancerek ...
Statistics for TWiki.Mizar Web Month: Topic views: Topic saves: File uploads: Most popular topic views: Top contributors for topic save ...
Rozdzia #322; 1: Artyku #322; Podstawow #261; jednostk #261; biblioteki MML jest artyku #322;. .
Podr #281;cznik Wersja angielska Mizar co to jest? Mizar jest proof checkerem wyposa #380;onym we w #322;asny j #281;zyk i bibliotek #281; artyku #322; #243;w ...
start Artyku #322; Artyku #322; Mizarowy to tekst ASSCI zawieraj #261;cy dwie cz #281; #347;ci: #347;rodowisko i tekst w #322;a #347;ciwy.
Definicja start Definicja zaczyna si #281; od s #322;owa kluczowego definition , a ko #324;czy si #281; s #322;owem end . Definicja zawiera deklaracj #281; locus ...
Generated abstract
Przeszukiwanie MML
Przyk #322;ady formalizacji Liczby naturalne
Przymiotnik
Tekst w #322;a #347;ciwy
Term
Uzasadnienie
Wzorzec
start Notacja Notacja to wzorzec konstruktor.
start Wzorce t #322;umaczenia
Schemat start Schemat to twierdzenie drugiego rz #281;du u #380;ywaj #261;ce zmiennych reprezentuj #261;xych formu #322;y i termy. Schemat zaczyna si #281; od s ...
start Cykl praxy z Mizarem Tekst artyku #322;u Mizarowego powstaje przy u #380;yciu edytora, np. emacsa. Co pewien czas wo #322;any jest weryfikator, który zaznacza ...
W #322;asno #347;ci start definition definition let x1 be Theta;1; let x1 be Theta;1; ...... .... ...
Formu #322;a atomowa start S #261; 4 typy formu #322;y atomowej: Predykatywna formu #322;a atomowa Ogólna posta #263;: 1, ..., k k 1, ..., ...
Abstrakt start Abstrakt to streszvczenie artyku #322;u zawieraj #261;ce eportowalne elementy: twierdzenia, schematy, definicje, rejestracje i wprowadzenia notacji ...
Formu #322;a start Formu #322;a jest zbudowana z formu #322; atomowych po #322; #261;czonych za pomoc #261; spójników logicznych: negacji not , koniunkcji , alternatywy ...
Konstruktor start Jest 7 rodzajów konstruktorów: Atrybut konstructor przymiotnika Funktor konstruktor termu Mode konstruktor type Predykat konstruktor formu #322 ...
start Rejestracja w #322;asno #347;ci sethood registration let x1 be Theta;1; ..... let xn be Theta;n; sethood of 1 ... m Theta;(x1,...,xn) proof ...
start Rejestracja identyczno #347;ci registration let x1 be Theta;1; ..... let xn be Theta;n; identify (a1,...,ak) (ak 1,...,am) with (b1,...,bj) ...
start Rejestracja redukcji registration let x1 be Theta;1; ..... let xn be Theta;n; reduce '; reducibility proof thus '; end; end ...
start Rejestracje Rejestracja egzystencjalna Rejestracja funktorowa Rejestracja identyczno #347;ci Rejestracja redukcji Rejestracja warunkowa ...
start Rejestracja warunkowa registration let x1 be Theta;1; ..... let xn be Theta;n; cluster 1 ... k 1 ... m for Theta;(x1,...,xn); coherence ...
start Rejestracja funktorowa registration let x1 be Theta;1; ..... let xn be Theta;n; cluster (x1,...,xn) 1 ... m; coherence proof :: thesis ...
start Rejestracja egzystencjalna registration let x1 be Theta;1; ..... let xn be Theta;n; cluster 1 ... m for Theta;(x1,...,xn); existence proof ...
start Funktor definition let x1 be Theta;1; ..... let xn be Theta;n; func (a1,...,am) (am 1,...,ak) #920;(x1,...,xn) means #934;(x1,...,xn ...
#346;rodowosko start #346;rodowisko zawiera dyrektywy importu z bazy MML. vocabularies notations constructors requirement registrations ...
Selector start Definicja struktury definition let x1 be Theta;1; ..... let xn be Theta;n; struct ( Sigma;1,..., Sigma;n) Sigma; over a1,...,am ( ...
Struktura start definition let x1 be Theta;1; ..... let xn be Theta;n; struct ( Sigma;1,..., Sigma;n) Sigma; over a1,...,am (# 1 Theta ...
Predykat start definition let x1 be Theta;1; ..... let xn be Theta;n; pred a1,...,am am 1,...,ak means Phi;(x1,...,xn,it); end; gdzie {a1,...,ak} ...
Funktor start definition let x1 be Theta;1; ..... let xn be Theta;n; mode of (a1,...,am) Theta;' means Phi;(x1,...,xn,it); end; definition let ...
Atrubut start definition let x1 be Theta;1; ..... let xn be Theta;n; attr xn is (a1,...,am) means Phi;(x1,...,xn); end; gdzie {a1,...,am} {x1,...,xn ...
Redefinicja start Redefinicja typu definition let x1 be Theta;1; ... let xn by Theta;n; redefine func (x1,...,xn) Theta;' of x1,...,xn; coherence ...
Warunki poprawno #347;ci start warunek znaczenie definicja/rejestracja existence istnieje obiekt odpowieniego typu spe #322;niaj #261;cy definins lub spe ...
Format start
Dowód start
Pragmaty start Pragmat ma posta #263; ::$X ....... gdzie X jest du #380; #261; liter #261;. ::$N nazwa elementu ::$EOF koniec pliku ::$P /::$P wy ...
Twierdzenie start Twierdzenie zawira s #322;owo kluczowe theorem , formu #322; #281; i uzasadnienie. Twierdzenie mo #380;e by #263; poprzedzone pragmatem z nazw ...
Taktyki dowodowe do g #211;ry Taktyki dowodowe zale #380; #261; od korelat #243;w semantycznych: korelat dowodzonej formu #322;y (z ewentualnymi rozwini #281;ciami ...
Articles that are being worked on: Author(s) Article Title Start Date Percent Complete Main.MarcoRiccardi MFOLD 3 Product of Manifolds. Tori. 2011 ...
Error Number: 9 Mizar Message: Too many instantiations Description Please contribute Typical examples environ vocabularies ZFMISC 1, PRE TOPC, EUCLID; constructors ...
nop is a subscription service to be automatically notified by email when topics change in the TWiki.Mizar web. This is a convenient service, so you do not have to ...
Inner product spaces and their generalizations, Hilbert spaces Primary classification # Article 1 bhsp 1 Introduction to Banach and Hilbert Spaces Part ...
Error Number: 93 Mizar Message: Missing field of a prefix Description While giving a definition to the structure one or more fields of the parent structure are omitted ...
Number of topics: 50
See also:
RSS feed, recent changes with 50, 100, 200, 500, 1000 topics, all changes Edit | Attach | Print version | History: r1 | Backlinks | Raw View | Raw edit | More topic actions
Topic revision: r1 - 2001-08-16 - 19:58:33 - PeterThoeny?
 |
|
Copyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors. Ideas, requests, problems regarding TWiki? Send feedback