Journal ArticleOPEN ACCESS

A Fully Automatic Theorem Prover with Human-Style Output

Journal of Automated Reasoning (2017) 58(2) 253-291
DOI: 10.1007/s10817-016-9377-1
37Citations
Citations of this article
18Readers
Mendeley users who have this article in their library.

This article is free to access.

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.

Author supplied keywords

Cite

CITATION STYLE

APA

Ganesalingam, M., & Gowers, W. T. (2017). A Fully Automatic Theorem Prover with Human-Style Output. Journal of Automated Reasoning, 58(2), 253–291. https://doi.org/10.1007/s10817-016-9377-1

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free