Accessibility navigation


Computer Theorem Proving and HoTT

Downloads

Downloads per month over past year

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

[img]
Preview
Text - Published Version
· Please see our End User Agreement before downloading.

449kB

Abstract/Summary

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
Refereed:Yes
Divisions:Faculty of Science
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

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

Page navigation