Edytor dowodów

Z Lem
Skocz do: nawigacji, wyszukiwania

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. zarzadzać logiką: zbierać aksjomaty i reguły wnioskowania
  6. zarzadzać 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.