A Fully Automatic Theorem Prover with Human-Style Output.
Published version
Peer-reviewed
Repository URI
Repository DOI
Type
Article
Change log
Authors
Ganesalingam, M
Gowers, WT
Abstract
This paper describes a program that solves elementary mathematical problems, mostly in metric space theory, and presents solutions that are hard to distinguish from solutions that might be written by human mathematicians.
Description
Keywords
ATP, Automated theorem proving, Human-like output, Human-oriented, Human-oriented theorem proving
Journal Title
J Autom Reason
Conference Name
Journal ISSN
0168-7433
1573-0670
1573-0670
Volume Title
Publisher
Springer Science and Business Media LLC
Publisher DOI
Sponsorship
Research supported by a Royal Society 2010 Anniversary Research Professorship.