Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
History of Interactive Theorem Proving

History of Interactive Theorem Proving

John Harrison, Josef Urban and Freek Wiedijk.

In Jörg Siekmann (ed), Handbook of the History of Logic, vol. 9: Computational Logic, Elsevier, pp. 135-214 (2014).

Abstract:

This book chapter gives a historical overview of the whole field of interactive theorem proving, with particular emphasis on the systems that introduced some of the key ideas that are still important.

PDF

Bibtex entry:

@INPROCEEDINGS{harrison-itp,
        author          = "John Harrison and Josef Urban and Freek Wiedijk",
        title           = "History of Interactive Theorem Proving",
        editor          = "J\{"o}rg Siekmann",
        booktitle       = "Handbook of the History of Logic vol. 9
                           (Computational Logic)",
        publisher       = "Elsevier",
        year            = 2014,
        pages           = "135--214"}