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 treści

• Artykuł
• Formułą
• Definicja
• Formalizacja

Spis alfabetyczny zagadnień

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

Konwerter polskich liter

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