We introduce PyEuclid, a unified and versatile Python-based formal system for representing and reasoning about plane geometry problems. PyEuclid designs a new formal language that faithfully encodes geometric information, including diagrams, and integrates two complementary components to perform geometric reasoning: (1) a deductive database with an extensive set of inference rules for geometric properties, and (2) an algebraic system for solving diverse equations involving geometric quantities. By seamlessly combining these components, PyEuclid enables human-like reasoning and supports generating concise reasoning steps (proofs), either fully automatically or through interactive guidance. Benchmark evaluations demonstrate that PyEuclid outperforms existing tools, solving a broader range of problems across both proof generation and calculation tasks. Moreover, PyEuclid holds significant potential for educational use and integration with advanced deep learning systems.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

PyEuclid: A Versatile Formal Plane Geometry System in Python

  • Zhaoyu Li,
  • Hangrui Bi,
  • Jialiang Sun,
  • Zenan Li,
  • Kaiyu Yang,
  • Xujie Si

摘要

We introduce PyEuclid, a unified and versatile Python-based formal system for representing and reasoning about plane geometry problems. PyEuclid designs a new formal language that faithfully encodes geometric information, including diagrams, and integrates two complementary components to perform geometric reasoning: (1) a deductive database with an extensive set of inference rules for geometric properties, and (2) an algebraic system for solving diverse equations involving geometric quantities. By seamlessly combining these components, PyEuclid enables human-like reasoning and supports generating concise reasoning steps (proofs), either fully automatically or through interactive guidance. Benchmark evaluations demonstrate that PyEuclid outperforms existing tools, solving a broader range of problems across both proof generation and calculation tasks. Moreover, PyEuclid holds significant potential for educational use and integration with advanced deep learning systems.