Proof-checker

Z Lem
Skocz do: nawigacji, wyszukiwania

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 LATEX-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.