Noriko H. Arai
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.
- T. Arai. Mathematical Logic. Iwanami Shoten, 2011. (in Japanese).Google Scholar
- A. Church. A note on the Entscheidungsproblem. Journal of Symbolic Logic, 1:40--41, 1936.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- K. Gödel. Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für Mathematik, 38(1):173--198, 1931.Google ScholarCross Ref
- T. C. Hales. The Jordan curve theorem, formally and informally. The American Mathematical Monthly, 114(10):882--894, 2007.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- 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.Google Scholar
- 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).Google Scholar
- J. Robinson. Definability and decision problems in arithmetic. The Journal of Symbolic Logic, 14(2):98--114, 1949.Google ScholarCross Ref
- M. Steedman. The Syntactic Process. Bradford Books. Mit Press, 2001. Google ScholarDigital Library
- A. W. Strzeboński. Cylindrical algebraic decomposition using validated numerics. Journal of Symbolic Computation, 41(9):1021--1038, 2006.Google ScholarCross Ref
- A. Tarski. A Decision Method for Elementary Algebra and Geometry. University of California Press, Berkeley, 1951.Google Scholar
- A. Turing. On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society, 42:230--265, 1936.Google Scholar
- A. N. Whitehead and B. A. W. Russell. Principia Mathematica. Cambridge Univ. Press, Cambridge, 1910, 1912, and 1913.Google Scholar
- L. Wittgenstein. Philosophical Investigations/Philosophische Untersuchungen. Oxford: Basil Blackwell, 1953.Google Scholar
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