Edytor dowodów: Różnice pomiędzy wersjami
Z Lem
(→To jest tymczasowa strona opisująca wymagania na Edytor Dowodów) |
|||
| Linia 3: | Linia 3: | ||
Edytor dowodów, lub inaczej asystent tworzenia dowodów. | Edytor dowodów, lub inaczej asystent tworzenia dowodów. | ||
| − | Zadania | + | Zadania edytora: |
# Prezentować dowód w postaci artykułu gotowego do druku. | # Prezentować dowód w postaci artykułu gotowego do druku. | ||
# Prezentować formuły w postaci | # Prezentować formuły w postaci | ||
| Linia 11: | Linia 11: | ||
#* tworzyć pomocnicze etykiety dla podformuł danej formuły | #* tworzyć pomocnicze etykiety dla podformuł danej formuły | ||
#* zwijać i rozwijac podformuły oznaczone etykietą | #* zwijać i rozwijac podformuły oznaczone etykietą | ||
| − | #* | + | #* 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ą: 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 | ||
Wersja z 15:55, 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 rozwijac 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
