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 5: Linia 5:
 
Zadania edytora:
 
Zadania edytora:
 
# Prezentować dowód  
 
# Prezentować dowód  
#* w postaci artykułu gotowego  do druku
+
#* w postaci artykułu gotowego  do druku, lub,
 
#* w postaci na tyle sformalizowanej, by można go przedstawić proof-checkerowi do weryfikacji.
 
#* 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ł

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