Edytor dowodów: Różnice pomiędzy wersjami
Z Lem
(→To jest tymczasowa strona opisująca wymagania na Edytor Dowodów) |
|||
| Linia 4: | Linia 4: | ||
Zadania edytora: | Zadania edytora: | ||
| − | # Prezentować dowód w postaci artykułu gotowego do druku. | + | # Prezentować dowód |
| + | #* w postaci artykułu gotowego do druku | ||
| + | #* 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 | ||
#* formuły | #* formuły | ||
# Wspomagać edycję formuł - przetwarzanie formuł | # Wspomagać edycję formuł - przetwarzanie formuł | ||
| − | #* tworzyć pomocnicze etykiety dla | + | #* tworzyć pomocnicze etykiety dla podwyrażeń danej formuły |
| − | #* zwijać i rozwijać | + | #* zwijać i rozwijać podwyrażenia oznaczone etykietą |
| − | #* dokonywać podstawień wewnątrz | + | #* 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 | ||
# zarządzać logiką: zbierać aksjomaty i reguły wnioskowania | # zarządzać logiką: zbierać aksjomaty i reguły wnioskowania | ||
| Linia 17: | Linia 19: | ||
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 | + | * 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 | + | * 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 | Przykłady | ||
# | # | ||
Wersja z 12:34, 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
- w postaci na tyle sformalizowanej, by można go przedstawić proof-checkerowi do weryfikacji.
- Prezentować formuły w postaci
- drzewa
- 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
