Podręcznik

Wersja angielska

Mizar - co to jest?

Mizar jest proof checkerem wyposażonym we własny język i bibliotekę artykułów matematycznych, które są publikowane w czasopiśmie Formalized Mathematics. Mizar nie jest proverem w tradycyjnym rozumieniu -- Mizar sprawdza poprawność formalizacji i rozumowań przeprowadzonych przez człowieka (zapisanych w Mizarze).

Spis alfabetyczny zagadnień

• Abstrakt^?
• Atrybut - konstruktor przymiotnika^?
• Cykl pracy (w Mizarze / z Mizarem)^?
• Definicja^?
• Format^?
• Formuła^?
• Funktor - konstruktor termu^?
• GAB - generalized abstract^? -- abstrakty uogólnione
• Gramatyka^?
• Konstruktor^?
• Korelaty semantyczne
• Mode - konstruktor typu^?
• Notacja^?
• Predykat - konstruktor formuły^?
• Przykłady prostych formalizacji^?
• Przeszukiwanie MML^?
• Przymiotnik^?
• Rejestracja^?
• Rejestracja egzystencjalna^?
• Rejestracja funktorowa^? (przymiotników termu)
• Rejestracja warunkowa^?
• Schemat^?
• Środowisko^?
• Taktyki dowodowe
• Tekst właściwy^?
• Term^?
• Typ^?
• Twierdzenie^?
• Warunek poprawności^?
• Własność^?
• Wzorzec^?
• Wzorzec tłumaczenia (FM)^?

Konwerter polskich liter

<META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=utf-8">

to top