Mathematics by machine

DOI10.1145/2608628.2627488MaRDI QIDQ3452371zbMATH OpenOpenAlexFDO

Authors Noriko H. Arai, Takuya Matsuzaki, Hidenao Iwane, Hirokazu Anai

Publication date 11 November 2015

Published in Proceedings of the 39th International Symposium on Symbolic and Algebraic Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2608628.2627488

zbMATH Keywords

mathematical logicnatural language processingquantifier elimination

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Quantifier elimination, model completeness, and related topics (03C10) Natural language processing (68T50)

Recommendations

• Mechanized Mathematics
• Mechanized mathematics
• scientific article; zbMATH DE number 1351869
• Machine mathematics: problems and prospects
• Mathematical machines: a laboratory for mathematics
• scientific article; zbMATH DE number 1782448
• scientific article; zbMATH DE number 1555236
• Machine-checked mathematics
• Towards the automatic mathematician

Cites work

• An effective implementation of symbolic-numeric cylindrical algebraic decomposition for quantifier elimination
• Cylindrical algebraic decomposition using validated numerics
• Definability and decision problems in arithmetic
• scientific article; zbMATH DE number 1952952 (Why is no real title available?)
• scientific article; zbMATH DE number 3068536 (Why is no real title available?)
• On Computable Numbers, with an Application to the Entscheidungsproblem
• The Jordan Curve Theorem, Formally and Informally

Cited in

(16)

• Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
• Using machine learning to improve cylindrical algebraic decomposition
• On multivariate Hermitian quadratic forms
• \textsf{SC}\(^2\): satisfiability checking meets symbolic computation. (Project paper)
• Race against the teens -- benchmarking mechanized math on pre-university problems
• Soft math math soft
• Discovering geometric theorems from scanned and photographed images of diagrams
• Machine synthesis of mathematical theorems
• scientific article; zbMATH DE number 4074439 (Why is no real title available?)
• scientific article; zbMATH DE number 622675 (Why is no real title available?)
• scientific article; zbMATH DE number 1782448 (Why is no real title available?)
• scientific article; zbMATH DE number 1870428 (Why is no real title available?)
• Can an A.I. win a medal in the mathematical olympiad? -- Benchmarking mechanized mathematics on pre-university problems
• Proof verification and proof discovery for relativity
• scientific article; zbMATH DE number 5030446 (Why is no real title available?)
• Mechanized mathematics

Describes a project that uses

Uses Software

• Jordan

This page was built for publication: Mathematics by machine

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3452371)