Literatura:
Interaktivni dokazivači:
The COQ Proof Assistant
Isabelle, generic proof assistant.
Lawrence Paulson: Isabelle - A Generic Theorem Prover, Springer
Benjamin Pierce: Software Foundations
Filip Maric: A Survey of Interactive Theorem Proving
Linkovi:
Masive Open Online Course (MOOC): Coursera
MIT OpenCourseWare