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.
2. Prezentować formuły w postaci
   • drzewa
   • formuły
3. Wspomagać edycję formuł - przetwarzanie formuł
   • tworzyć pomocnicze etykiety dla podformuł danej formuły
   • zwijać i rozwijać podformuły oznaczone etykietą
   • dokonywać podstawień wewnątrz podformuły
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żnosci od zadania jakie jest rozwiazywane.
• wykorzystywać rdzenie procesora do uruchamiania wątków. Pewne watki mogłyby zajmować się poszukiwaniem możliwych do zastosowania operacji na formule jaką przetwarzamy.

Przykłady