Proof-checker: Różnice pomiędzy wersjami
Z Lem
(Utworzył nową stronę „== Uwagi nt. proof-checkera. == # Proof-checker powinien być zdolny do analizy tekstów przygotowanych przez edytor dowodów. # Analizowany dowód składa się z fo...”) |
(→Uwagi nt. proof-checkera.) |
||
| Linia 1: | Linia 1: | ||
== Uwagi nt. proof-checkera. == | == Uwagi nt. proof-checkera. == | ||
# Proof-checker powinien być zdolny do analizy tekstów przygotowanych przez edytor dowodów. | # Proof-checker powinien być zdolny do analizy tekstów przygotowanych przez edytor dowodów. | ||
| − | # Analizowany dowód składa się z formuł algorytmicznych oddzielanych tekstem. | + | # Analizowany dowód składa się z formuł '''algorytmicznych''' oddzielanych tekstem. Format L<sup>A</sup>T<sub>E</sub>X-owy lub podobny? |
| − | Format L<sup>A</sup>T<sub>E</sub>X-owy lub podobny? | + | |
# Tekst służy organizowaniu dowodu w strukturę drzewa. | # Tekst służy organizowaniu dowodu w strukturę drzewa. | ||
| − | # | + | # W odróżnieniu od Mizara powinniśmy zacząć pracę od zebrania zbioru twierdzeń. Zbiór ten powinien mieć strukturę, np. twierdzenia odnoszące się do struktury liczb naturalnych, twierdzenia o stosach, o drzewach binarnych poszukiwań, etc. |
Aktualna wersja na dzień 09:32, 14 mar 2013
Uwagi nt. proof-checkera.
- Proof-checker powinien być zdolny do analizy tekstów przygotowanych przez edytor dowodów.
- Analizowany dowód składa się z formuł algorytmicznych oddzielanych tekstem. Format LATEX-owy lub podobny?
- Tekst służy organizowaniu dowodu w strukturę drzewa.
- W odróżnieniu od Mizara powinniśmy zacząć pracę od zebrania zbioru twierdzeń. Zbiór ten powinien mieć strukturę, np. twierdzenia odnoszące się do struktury liczb naturalnych, twierdzenia o stosach, o drzewach binarnych poszukiwań, etc.
