Proof-checker

Z Lem
Wersja AndrzejSalwicki (dyskusja | edycje) z dnia 09:32, 14 mar 2013

(różn.) ← poprzednia wersja | przejdź do aktualnej wersji (różn.) | następna wersja → (różn.)
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.