Proof-checker

Uwagi nt. proof-checkera.

1. Proof-checker powinien być zdolny do analizy tekstów przygotowanych przez edytor dowodów.
2. Analizowany dowód składa się z formuł algorytmicznych oddzielanych tekstem. Format L^AT_EX-owy lub podobny?
3. Tekst służy organizowaniu dowodu w strukturę drzewa.
4. 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.