Euclidean Geometry by High-performance Solvers?

dc.contributor.author	Gadgil, Siddhartha	en_US
dc.contributor.author	TADIPATRI, ANAND	en_US
dc.date.accessioned	2023-04-27T10:11:19Z
dc.date.available	2023-04-27T10:11:19Z
dc.date.issued	2022-05	en_US
dc.identifier.citation	Resonance, 27(5), 801–816.	en_US
dc.identifier.issn	0971-8044	en_US
dc.identifier.issn	0973-712X	en_US
dc.identifier.uri	https://doi.org/10.1007/s12045-022-1373-7	en_US
dc.identifier.uri	http://dr.iiserpune.ac.in:8080/xmlui/handle/123456789/7768
dc.description.abstract	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.	en_US
dc.language.iso	en	en_US
dc.publisher	Indian Academy of Sciences	en_US
dc.subject	Automated theorem proving	en_US
dc.subject	Euclidean geometry	en_US
dc.subject	SMT solvers	en_US
dc.subject	2022	en_US
dc.title	Euclidean Geometry by High-performance Solvers?	en_US
dc.type	Article	en_US
dc.contributor.department	Dept. of Mathematics	en_US
dc.identifier.sourcetitle	Resonance	en_US
dc.publication.originofpublisher	Indian	en_US