Edytor dowodów: Różnice pomiędzy wersjami
Z Lem
| Linia 9: | Linia 9: | ||
#* formuły | #* formuły | ||
# Wspomagać edycję formuł - przetwarzanie formuł | # Wspomagać edycję formuł - przetwarzanie formuł | ||
| + | #* tworzyć pomocnicze etykiety dla podformuł danej formuły | ||
| + | #* zwijać i rozwijac podformuły oznaczone etykietą | ||
| + | #* dokonywac podstawień wewnatrz podformuły | ||
# Wspomagać - wyszukiwać reguły wnioskowania, które mogą być zastosowane | # Wspomagać - wyszukiwać reguły wnioskowania, które mogą być zastosowane | ||
| − | # | + | # zarzadzać logiką: aksjomaty i reguły wnioskowania |
| + | # zarzadzać bazą wiedzy - zbiorem twierdzeń i definicji | ||
Wersja z 12:12, 13 mar 2013
To jest tymczasowa strona opisująca wymagania na Edytor Dowodów
Edytor dowodów, lub inaczej asystent tworzenia dowodów.
Zadania
- 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 rozwijac podformuły oznaczone etykietą
- dokonywac podstawień wewnatrz podformuły
- Wspomagać - wyszukiwać reguły wnioskowania, które mogą być zastosowane
- zarzadzać logiką: aksjomaty i reguły wnioskowania
- zarzadzać bazą wiedzy - zbiorem twierdzeń i definicji
