Edytor dowodów: Różnice pomiędzy wersjami

Z Lem
Skocz do: nawigacji, wyszukiwania
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

  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 rozwijac podformuły oznaczone etykietą
    • dokonywac podstawień wewnatrz podformuły
  4. Wspomagać - wyszukiwać reguły wnioskowania, które mogą być zastosowane
  5. zarzadzać logiką: aksjomaty i reguły wnioskowania
  6. zarzadzać bazą wiedzy - zbiorem twierdzeń i definicji