research-article

Mathematics by machine

Authors:

Noriko H. Arai,

Takuya Matsuzaki,

Hirokazu AnaiAuthors Info & Claims

ISSAC '14: Proceedings of the 39th International Symposium on Symbolic and Algebraic Computation

Pages 1 - 8

https://doi.org/10.1145/2608628.2627488

Published: 23 July 2014 Publication History

Abstract

When David Hilbert started so called "Hilbert's program" (formalization of mathematics) in the early 20th century to give a solid foundation to mathematics, he unintentionally introduced the possibility of automatization of mathematics. Theoretically, the possibility was denied by Gödel's incompleteness theorem. However, an interesting issue remains: is "mundane mathematics" automatizable? We are developing a system that solves a wide range of math problems written in natural language, as a part of the Todai Robot Project, an AI challenge to pass the university entrance examination. We give an overview and report on the progress of our project, and the theoretical and methodological difficulties to be overcome.

References

[1]

T. Arai. Mathematical Logic. Iwanami Shoten, 2011. (in Japanese).

[2]

A. Church. A note on the Entscheidungsproblem. Journal of Symbolic Logic, 1:40--41, 1936.

[3]

G. E. Collins. Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In Automata Theory and Formal Languages 2nd GI Conference Kaiserslautern, volume 33 of Lecture Notes in Computer Science, pages 134--183. Springer-Verlag, 1975.

Digital Library

[4]

K. Gödel. Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für Mathematik, 38(1):173--198, 1931.

[5]

T. C. Hales. The Jordan curve theorem, formally and informally. The American Mathematical Monthly, 114(10):882--894, 2007.

[6]

H. Iwane, H. Yanami, H. Anai, and K. Yokoyama. An effective implementation of symbolic-numeric cylindrical algebraic decomposition for quantifier elimination. Theoretical Computer Science, 479:43--69, 2013.

Digital Library

[7]

T. Matsuzaki, H. Iwane, H. Anai, and N. Arai. The complexity of math problems -- linguistic, or computational? In Proceedings of the Sixth International Joint Conference on Natural Language Processing, pages 73--81, 2013.

[8]

T. Matsuzaki, H. Iwane, H. Anai, and N. H. Arai. The most uncreative examinee: a first step toward wide coverage natural language math problem solving. In Proceedings of the 28th AAAI Conference on Artificial Intelligence, 2014. (to appear).

[9]

J. Robinson. Definability and decision problems in arithmetic. The Journal of Symbolic Logic, 14(2):98--114, 1949.

[10]

M. Steedman. The Syntactic Process. Bradford Books. Mit Press, 2001.

Digital Library

[11]

A. W. Strzeboński. Cylindrical algebraic decomposition using validated numerics. Journal of Symbolic Computation, 41(9):1021--1038, 2006.

[12]

A. Tarski. A Decision Method for Elementary Algebra and Geometry. University of California Press, Berkeley, 1951.

[13]

A. Turing. On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society, 42:230--265, 1936.

[14]

A. N. Whitehead and B. A. W. Russell. Principia Mathematica. Cambridge Univ. Press, Cambridge, 1910, 1912, and 1913.

[15]

L. Wittgenstein. Philosophical Investigations/Philosophische Untersuchungen. Oxford: Basil Blackwell, 1953.

Cited By

Bradford RDavenport JEngland MSadeghimanesh AUncu A(2022)The DEWCAD projectACM Communications in Computer Algebra10.1145/3511528.351153855:3(107-111)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3511528.3511538
Ábrahám EDavenport JEngland MKremer G(2020)Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coveringsJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2020.100633(100633)Online publication date: Nov-2020
https://doi.org/10.1016/j.jlamp.2020.100633
Huang ZEngland MWilson DBridge JDavenport JPaulson L(2019)Using Machine Learning to Improve Cylindrical Algebraic DecompositionMathematics in Computer Science10.1007/s11786-019-00394-8Online publication date: 3-Apr-2019
https://doi.org/10.1007/s11786-019-00394-8
Show More Cited By

Index Terms

Mathematics by machine

Recommendations

Completeness and Cut-elimination in the Intuitionistic Theory of Types

In this paper we define a model theory and give a semantic proof of cut-elimination for ICTT, an intuitionistic formulation of Church's theory of types defined by Miller et al. and the basis for the λProlog programming language. Our approach, extending ...
Computing Circumscription Revisited: A Reduction Algorithm

In recent years, a great deal of attention has been devoted to logics of common-sense reasoning. Among the candidates proposed, circumscription has been perceived as an elegant mathematical technique for modeling nonmonotonic reasoning, but difficult to ...
Quantified epistemic logics for reasoning about knowledge in multi-agent systems

We introduce quantified interpreted systems, a semantics to reason about knowledge in multi-agent systems in a first-order setting. Quantified interpreted systems may be used to interpret a variety of first-order modal epistemic languages with global ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

ISSAC '14: Proceedings of the 39th International Symposium on Symbolic and Algebraic Computation

July 2014

444 pages

ISBN:9781450325011

DOI:10.1145/2608628

Editor:
Katsusuke Nabeshima
The University of Tokushima, Japan
,
General Chairs:
Kosaku Nagasaka
Kobe University, Japan
,
Franz Winkler
RISC, University Linz, Austria
,
Program Chair:
Agnes Szanto
North Carolina State University

Copyright © 2014 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 July 2014

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ISSAC '14

ISSAC '14: International Symposium on Symbolic and Algebraic Computation

July 23 - 25, 2014

Kobe, Japan

Acceptance Rates

ISSAC '14 Paper Acceptance Rate 51 of 96 submissions, 53%;

Overall Acceptance Rate 395 of 838 submissions, 47%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
236
Total Downloads

Downloads (Last 12 months)17
Downloads (Last 6 weeks)2

Reflects downloads up to 26 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Bradford RDavenport JEngland MSadeghimanesh AUncu A(2022)The DEWCAD projectACM Communications in Computer Algebra10.1145/3511528.351153855:3(107-111)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3511528.3511538
Ábrahám EDavenport JEngland MKremer G(2020)Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coveringsJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2020.100633(100633)Online publication date: Nov-2020
https://doi.org/10.1016/j.jlamp.2020.100633
Huang ZEngland MWilson DBridge JDavenport JPaulson L(2019)Using Machine Learning to Improve Cylindrical Algebraic DecompositionMathematics in Computer Science10.1007/s11786-019-00394-8Online publication date: 3-Apr-2019
https://doi.org/10.1007/s11786-019-00394-8
Sato YFukasaku RSekigawa HKauers MOvchinnikov ASchost É(2018)On Continuity of the Roots of a Parametric Zero Dimensional Multivariate Polynomial IdealProceedings of the 2018 ACM International Symposium on Symbolic and Algebraic Computation10.1145/3208976.3209004(359-365)Online publication date: 11-Jul-2018
https://dl.acm.org/doi/10.1145/3208976.3209004
Fukasaku RIwane HSato Y(2018)On Multivariate Hermitian Quadratic FormsMathematics in Computer Science10.1007/s11786-018-0387-813:1-2(79-93)Online publication date: 12-Oct-2018
https://doi.org/10.1007/s11786-018-0387-8
Matsuzaki T(2017)Language Processing of Mathematical Problem Text数学問題の自然言語解析Kagaku tetsugaku10.4216/jpssj.50.0_3550(35-49)Online publication date: 20-Dec-2017
https://doi.org/10.4216/jpssj.50.0_35
Iwane HAnai HYap CEl Din M(2017)Formula Simplification for Real Quantifier Elimination Using Geometric InvarianceProceedings of the 2017 ACM International Symposium on Symbolic and Algebraic Computation10.1145/3087604.3087627(213-220)Online publication date: 23-Jul-2017
https://dl.acm.org/doi/10.1145/3087604.3087627
Ábrahám EAbbott JBecker BBigatti ABrain MBuchberger BCimatti ADavenport JEngland MFontaine PForrest SGriggio AKroening DSeiler WSturm T(2016)$$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic ComputationIntelligent Computer Mathematics10.1007/978-3-319-42547-4_3(28-43)Online publication date: 12-Jul-2016
https://doi.org/10.1007/978-3-319-42547-4_3
Wada YMatsuzaki TTerui AArai N(2016)An Automated Deduction and Its Implementation for Solving Problem of Sequence at University Entrance ExaminationMathematical Software – ICMS 201610.1007/978-3-319-42432-3_11(82-89)Online publication date: 6-Jul-2016
https://doi.org/10.1007/978-3-319-42432-3_11
Fukasaku RIwane HSato YRobertz DLinton SYokoyama K(2015)Real Quantifier Elimination by Computation of Comprehensive Gröbner SystemsProceedings of the 2015 ACM International Symposium on Symbolic and Algebraic Computation10.1145/2755996.2756646(173-180)Online publication date: 24-Jun-2015
https://dl.acm.org/doi/10.1145/2755996.2756646
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents