Euclidean Geometry by High-performance Solvers?

Resonance

article

Siddhartha Gadgil¹  Anand Tadipatri² 

[1] Department of Mathematics, Indian Institute of Science;Indian Institute of Science Education and Research

关键词: Automated theorem proving;    Euclidean geometry;    SMT solvers.;   

DOI  :  10.1007/s12045-022-1373-7

学科分类：社会科学、人文和艺术（综合）

来源: Springer

【 摘 要 】

Tarski showed in the 1950s that (first-order) questions in Euclidean geometry could be answered algorithmically. Algorithms for doing this have greatly improved over the decades but still have high complexity (in terms of time taken). We experiment using state-of-the-art software, specifically so-called $SMT Solvers$, to see how practical it is to prove classical Euclidean geometry results in this way.

【 授权许可】

Others