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:

Prezentować dowód
- w postaci artykułu gotowego do druku, lub,
- w postaci na tyle sformalizowanej, by można go przedstawić proof-checkerowi do weryfikacji.
Prezentować formuły w postaci
- drzewa lub
- formuły
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ń
Wspomagać - wyszukiwać reguły wnioskowania, które mogą być zastosowane
zarządzać logiką: zbierać aksjomaty i reguły wnioskowania
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 Tu parę nieudolnych przykładów, które maja zilustrować co mam na myśli.