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

Z Lem
Skocz do: nawigacji, wyszukiwania
 
(Nie pokazano 5 pośrednich wersji utworzonych przez tego samego użytkownika)
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, lub,
 +
#* w postaci na tyle sformalizowanej, by można go przedstawić proof-checkerowi do weryfikacji.
 
# Prezentować formuły w postaci
 
# Prezentować formuły w postaci
#* drzewa
+
#* drzewa lub
 
#* formuły
 
#* formuły
 
# Wspomagać edycję formuł - przetwarzanie formuł
 
# Wspomagać edycję formuł - przetwarzanie formuł
#* tworzyć pomocnicze etykiety dla podformuł danej formuły
+
#* tworzyć pomocnicze etykiety dla podwyrażeń danej formuły
#* zwijać i rozwijac podformuły oznaczone etykietą
+
#* zwijać i rozwijać podwyrażenia oznaczone etykietą
#* dokonywac podstawień wewnatrz podformuły
+
#* dokonywać podstawień wewnątrz podwyrażeń
 
# 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
+
# 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:
 +
* 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żności od zadania jakie jest rozwiązywane.
 +
* wykorzystywać rdzenie procesora do uruchamiania wątków. Pewne wątki mogłyby zajmować się poszukiwaniem możliwych do zastosowania operacji na formule jaką przetwarzamy.
 +
 
 +
Przykłady
 +
Tu parę nieudolnych przykładów, które maja zilustrować co mam na myśli.
 +
#http://lem12.uksw.edu.pl/images/8/8b/BST-Próba-dowodu.pdf
 +
#

Aktualna wersja na dzień 14:41, 3 kwi 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, lub,
    • w postaci na tyle sformalizowanej, by można go przedstawić proof-checkerowi do weryfikacji.
  2. Prezentować formuły w postaci
    • drzewa lub
    • formuły
  3. Wspomagać edycję formuł - przetwarzanie formuł
    • tworzyć pomocnicze etykiety dla podwyrażeń danej formuły
    • zwijać i rozwijać podwyrażenia oznaczone etykietą
    • dokonywać podstawień wewnątrz podwyrażeń
  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żności od zadania jakie jest rozwiązywane.
  • wykorzystywać rdzenie procesora do uruchamiania wątków. Pewne wątki mogłyby zajmować się poszukiwaniem możliwych do zastosowania operacji na formule jaką przetwarzamy.

Przykłady Tu parę nieudolnych przykładów, które maja zilustrować co mam na myśli.

  1. http://lem12.uksw.edu.pl/images/8/8b/BST-Próba-dowodu.pdf