Edytor dowodów: Różnice pomiędzy wersjami
Z Lem
(→To jest tymczasowa strona opisująca wymagania na Edytor Dowodów) |
|||
| Linia 10: | Linia 10: | ||
# Wspomagać edycję formuł - przetwarzanie formuł | # Wspomagać edycję formuł - przetwarzanie formuł | ||
#* tworzyć pomocnicze etykiety dla podformuł danej formuły | #* tworzyć pomocnicze etykiety dla podformuł danej formuły | ||
| − | #* zwijać i | + | #* zwijać i rozwijać podformuły oznaczone etykietą |
#* dokonywać podstawień wewnątrz podformuły | #* dokonywać podstawień wewnątrz podformuły | ||
# Wspomagać - wyszukiwać reguły wnioskowania, które mogą być zastosowane | # Wspomagać - wyszukiwać reguły wnioskowania, które mogą być zastosowane | ||
# zarzadzać logiką: zbierać aksjomaty i reguły wnioskowania | # zarzadzać logiką: zbierać aksjomaty i reguły wnioskowania | ||
# zarzadzać bazą wiedzy - zbiorem twierdzeń i definicji | # 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. | ||
Wersja z 17:05, 13 mar 2013
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.
- Prezentować formuły w postaci
- drzewa
- formuły
- 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
- Wspomagać - wyszukiwać reguły wnioskowania, które mogą być zastosowane
- zarzadzać logiką: zbierać aksjomaty i reguły wnioskowania
- 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.
