Advanced Search
    Zhang Jingzhong, Zhang Chuanjun, Zheng Huan, Rao Yongsheng, Zou Yu. The Realization and Application of Symbolic Computation Modules in SGARP[J]. Journal of Computer Research and Development, 2014, 51(6): 1341-1351.
    Citation: Zhang Jingzhong, Zhang Chuanjun, Zheng Huan, Rao Yongsheng, Zou Yu. The Realization and Application of Symbolic Computation Modules in SGARP[J]. Journal of Computer Research and Development, 2014, 51(6): 1341-1351.

    The Realization and Application of Symbolic Computation Modules in SGARP

    • SGARP (sustainable geometry automated reasoning platform) enables users to add or change the knowledge involved in automated geometry theorem proving, such as geometry objects, predicates, theorems or reasoning rules, so that varieties of rule-based machine proving methods or human-machine interactive reasoning methods could be developed. In order to further enhance the automated reasoning power of SGARP and to expand its scope of application, this paper proposes a convenient way of implementing the symbolic computation modules in SGARP. Based on the embedded symbolic computation modules, the mass point method and the analytic method are successfully added into SGARP. The mass point method can prove the Hilbert intersection point statements, and the analytic method can assist in proving all types of difficult geometric theorems, such as the famous Thebault's Theorem. As for the two embedded methods, we test them with 180 geometry problems in TGTP (thousands of geometric problems for geometric theorem provers) which is a Web-based library of problems in geometry. The results show that all of the 180 geometry problems could be proved within a reasonable time with readable machine proofs, which shows that the upgraded SGARP can better satisfy the users' requirements for learning and developing automated geometry reasoning.
    • loading

    Catalog

      Turn off MathJax
      Article Contents

      /

      DownLoad:  Full-Size Img  PowerPoint
      Return
      Return