Edytor dowodów

To jest tymczasowa strona opisująca wymagania na Edytor Dowodów

Edytor dowodów, lub inaczej asystent tworzenia dowodów.

Zadania edytora:

1. Prezentować dowód
   • w postaci artykułu gotowego do druku
   • w postaci na tyle sformalizowanej, by można go przedstawić proof-checkerowi do weryfikacji.
2. Prezentować formuły w postaci
   • drzewa
   • formuły
3. Wspomagać edycję formuł - przetwarzanie formuł
   • tworzyć pomocnicze etykiety dla podwyrażeń danej formuły
   • zwijać i rozwijać podwyrażenia oznaczone etykietą
   • dokonywać podstawień wewnątrz podwyrażeń
4. Wspomagać - wyszukiwać reguły wnioskowania, które mogą być zastosowane
5. zarządzać logiką: zbierać aksjomaty i reguły wnioskowania
6. zarządzać bazą wiedzy - zbiorem twierdzeń i definicji

Pomysły:

• używać ANTLR do budowy kolejnych analizatorów składniowych - kolejnych, ponieważ podczas pracy nad weryfikacją oprogramowania często zmieniamy język. Zbiory funktorów i predykatów zmieniają się w zależności od zadania jakie jest rozwiązywane.
• wykorzystywać rdzenie procesora do uruchamiania wątków. Pewne wątki mogłyby zajmować się poszukiwaniem możliwych do zastosowania operacji na formule jaką przetwarzamy.

Przykłady