A Machine Proof System of Point Geometry Based on Coq

Siran Lei, Hao Guan, Jianguo Jiang, Yu Zou and Yongsheng Rao ()
Additional contact information
Siran Lei: Institute of Computing Science and Technology, Guangzhou University, Guangzhou 510006, China
Hao Guan: Institute of Computing Science and Technology, Guangzhou University, Guangzhou 510006, China
Jianguo Jiang: School of Mathematics, Liaoning Normal University, Dalian 116029, China
Yu Zou: Institute of Computing Science and Technology, Guangzhou University, Guangzhou 510006, China
Yongsheng Rao: Institute of Computing Science and Technology, Guangzhou University, Guangzhou 510006, China

Mathematics, 2023, vol. 11, issue 12, 1-16

Abstract: An important development in geometric algebra in recent years is the new system known as point geometry, which treats points as direct objects of operations and considerably simplifies the process of geometric reasoning. In this paper, we provide a complete formal description of the point geometry theory architecture and give a rigorous and reliable formal verification of the point geometry theory based on the theorem prover Coq. Simultaneously, a series of tactics are also designed to assist in the proof of geometric propositions. Based on the theoretical architecture and proof tactics, a universal and scalable interactive point geometry machine proof system, PointGeo, is built. In this system, any arbitrary point-geometry-solvable geometric statement may be proven, along with readable information about the solution’s procedure. Additionally, users may augment the rule base by adding trustworthy rules as needed for certain issues. The implementation of the system expands the library of Coq resources on geometric algebra, which will become a significant research foundation for the fields of geometric algebra, computer science, mathematics education, and other related fields.

Keywords: point geometry; formal method; interact theorem proving; Coq; machine proof (search for similar items in EconPapers)
JEL-codes: C (search for similar items in EconPapers)
Date: 2023
References: View references in EconPapers View complete reference list from CitEc
Citations:

Downloads: (external link)
https://www.mdpi.com/2227-7390/11/12/2757/pdf (application/pdf)
https://www.mdpi.com/2227-7390/11/12/2757/ (text/html)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:gam:jmathe:v:11:y:2023:i:12:p:2757-:d:1173653

Access Statistics for this article

Mathematics is currently edited by Ms. Emma He

More articles in Mathematics from MDPI
Bibliographic data for series maintained by MDPI Indexing Manager ().