Edytor dowodów: Różnice pomiędzy wersjami
Z Lem
(→To jest tymczasowa strona opisująca wymagania na Edytor Dowodów) |
|||
| Linia 13: | Linia 13: | ||
#* dokonywać podstawień wewnątrz podformuły | #* dokonywać podstawień wewnątrz podformuły | ||
# 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: | 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żnosci od zadania jakie jest rozwiazywane. | * 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żnosci od zadania jakie jest rozwiazywane. | ||
* wykorzystywać rdzenie procesora do uruchamiania wątków. Pewne watki mogłyby zajmować się poszukiwaniem możliwych do zastosowania operacji na formule jaką przetwarzamy. | * wykorzystywać rdzenie procesora do uruchamiania wątków. Pewne watki mogłyby zajmować się poszukiwaniem możliwych do zastosowania operacji na formule jaką przetwarzamy. | ||
| + | |||
| + | Przykłady | ||
| + | # | ||
Wersja z 16:06, 13 mar 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.
- Prezentować formuły w postaci
- drzewa
- formuły
- Wspomagać edycję formuł - przetwarzanie formuł
- tworzyć pomocnicze etykiety dla podformuł danej formuły
- zwijać i rozwijać podformuły oznaczone etykietą
- dokonywać podstawień wewnątrz podformuły
- 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żnosci od zadania jakie jest rozwiazywane.
- wykorzystywać rdzenie procesora do uruchamiania wątków. Pewne watki mogłyby zajmować się poszukiwaniem możliwych do zastosowania operacji na formule jaką przetwarzamy.
Przykłady
