Edytor dowodów: Różnice pomiędzy wersjami
Z Lem
| (Nie pokazano 1 pośredniej wersji utworzonej przez tego samego użytkownika) | |||
| 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ł | ||
| Linia 23: | Linia 23: | ||
Przykłady | 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:
- 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
- drzewa lub
- formuły
- 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ń
- Wspomagać - wyszukiwać reguły wnioskowania, które mogą być zastosowane
- zarządzać logiką: zbierać aksjomaty i reguły wnioskowania
- 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.
