Wyniki wyszukiwania - BazTech

Ograniczanie wyników

Znaleziono wyników: 1

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: repozytoria sformalizowanej matematyki

Sortuj według:

Ogranicz wyniki do:

Exploring MiZAR library with MML Query

Bancerek G.

Zeszyty Naukowe Politechniki Białostockiej. Informatyka

2007

Z. 2

5-18

MiZAR, a proof-checking system, is used to build the MiZAR Mathematical Li-brary (MML). MML Query is a semantics-based tool for managing the mathematical knowl-edge in MiZAR including searching, browsing and presentation of the evolving MML content. The tool is becoming widely used as an aid for MiZAR authors and plays an essential role in the ongoing reorganization of MML. In the paper, we briefly present MiZAR system including language, tools for logical verifi-cation and publishing, foundations of MML, its content and maintenance, and the problems raising when using the MML (information retrieval and rendering). We also present the pos-sibilities offered by MML Query to solve these problems.

MlZAR(komputerowy system weryfikacji dowodów) jest używany do budowania MiZAR Mathematical Library (MML). MML Query jest narzędziem opartym o semantykę tekstu mizarowego służącym do zarządzania wiedzą w systemie MiZAR włączając w to wyszukiwanie, przeglądanie i prezentację ewolującej zawartości MML. Narzędzie to stało się szeroko używane jako pomoc dla autorów mizarowych oraz odgrywa istotną rolę w nieustających reorganizacjach MML. W artykule zaprezentowane są elementy systemu MiZAR i MML Query jak język, narzędzia logicznej weryfikacji i automatycznej publikacji, podstawy biblioteki MML, jej zawartość i konserwacja oraz problemy pojawiające się przy używaniu MML (odzyskiwanie informacji orazjej przedstawianie). Ponadto, są przedstawione możliwości MMLQuery w rozwiązywaniu tych problemów.