Edytor dowodów: Różnice pomiędzy wersjami
Z Lem
| (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 | + | #* tworzyć pomocnicze etykiety dla podwyrażeń danej formuły |
| − | #* zwijać i | + | #* zwijać i rozwijać podwyrażenia oznaczone etykietą |
| − | #* | + | #* 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ć 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:
- 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.
