Accessibility navigation

Computer Theorem Proving and HoTT

Leslie-Hurd, J. and Haworth, G. ORCID: (2013) Computer Theorem Proving and HoTT. ICGA Journal, 36 (2). pp. 100-103. ISSN 1389-6911

Text - Published Version
· Please see our End User Agreement before downloading.


It is advisable to refer to the publisher's version if you intend to cite from this work. See Guidance on citing.


Theorem-proving is a one-player game. The history of computer programs being the players goes back to 1956 and the ‘LT’ LOGIC THEORY MACHINE of Newell, Shaw and Simon. In game-playing terms, the ‘initial position’ is the core set of axioms chosen for the particular logic and the ‘moves’ are the rules of inference. Now, the Univalent Foundations Program at IAS Princeton and the resulting ‘HoTT’ book on Homotopy Type Theory have demonstrated the success of a new kind of experimental mathematics using computer theorem proving.

Item Type:Article
ID Code:33158
Uncontrolled Keywords:Axiom of Choice, automated theorem proving, computer theorem proving, HoTT, Homotopy Type Theory, IAS, LT, Logic Theory Machine, Princeton, Univalent Foundations Program, Voevodsky
Publisher:The International Computer Games Association


Downloads per month over past year

University Staff: Request a correction | Centaur Editors: Update this record

Page navigation