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

Z Lem
Skocz do: nawigacji, wyszukiwania
(To jest tymczasowa strona opisująca wymagania na Edytor Dowodów)
Linia 13: Linia 13:
 
#* 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
+
# zarządzać logiką: zbierać aksjomaty i reguły wnioskowania
# zarzadzać bazą wiedzy - zbiorem twierdzeń i definicji
+
# zarządzać bazą wiedzy - zbiorem twierdzeń i definicji
  
 
Pomysły:
 
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.
 
* 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.
 
* wykorzystywać rdzenie procesora do uruchamiania wątków. Pewne watki mogłyby zajmować się poszukiwaniem możliwych do zastosowania operacji na formule jaką przetwarzamy.
 +
 +
Przykłady
 +
#

Wersja z 16:06, 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:

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

Przykłady