GO-001
2015-07-14
2022-09-30
Rozwój systemu Mizar oraz Mizar Mathematical Library
dr Adam Naumowicz
Projekt dotyczy wykorzystania zasobów klastra obliczeniowego do dalszego rozwoju systemu interaktywnego dowodzenia twierdzeń matematycznych Mizar oraz zarządzania dużym repozytorium zgromadzonych faktów matematycznych wraz z ich dowodami, Mizar Mathematical Library (MML). W ramach projektu będzie prowadzona systematyczna analiza istniejącej bazy przy użyciu dostępnych zasobów obliczeniowych. Określone zostaną kryteria integralności oraz zaimplementowane narzędzia wspomagające detekcję błędów oraz eksplorację zgromadzonej wiedzy. Prowadzone będą też prace polegające na projektowaniu nowych i doskonaleniu istniejących algorytmów wykorzystywanych przez moduły systemu weryfikującego. Przeprowadzenie licznych eksperymentów testujących nowe algorytmy wymaga dostępu do mocy obliczeniowych znacznie przekraczających możliwości pojedynczych komputerów. Również wzmacnianie siły dedukcyjnej systemu jest kosztowne obliczeniowo, jednak może wykorzystywać mechanizmy przetwarzania równoległego. Doskonalone będą w tym celu metody efektywnego zrównoleglania Mizara. Jednocześnie wykonane zostaną eksperymenty nad MML z wykorzystaniem opracowanych modułów, w szczególności poprzez tworzenie nowych artykułów oraz refaktoryzację wcześniej skolekcjonowanych w repozytorium prac. Ich rezultaty pozwolą na gromadzenie statystyk służących do przeprowadzenia analizy ich użyteczności i efektywności. Przygotowana baza danych będzie mogła być również wykorzystywana w badaniach nad rozwojem systemów automatycznego dowodzenia twierdzeń (proverów) ze szczególnym uwzględnieniem metod uczenia maszynowego i sztucznej inteligencji. Po każdej modyfikacji bazy będzie następowała pełna weryfikacja zgromadzonej wiedzy oraz zależności pomiędzy artykułami wchodzącymi w skład repozytorium. Analizowane będą zmiany rozmiaru tekstów, czasu ich przetwarzania oraz związane z tym wymagania pamięciowe oprogramowania systemowego. Wyniki tych badań posłużą do określenia głównych kierunków rozwoju zarówno MML jak też języka i systemu weryfikującego. Możliwie szybkie i rutynowe generowaniu aktualnych wersji bazy MML oraz eksperymenty i prace wdrożeniowe nowych modułów również wymagają dostępu do wydajnych serwerów.