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.

Many problems of practical interest can be modeled and solved by using interval-valued fuzzy graph (IVFG) algorithms. An IVFG is a very useful and effective tool for studying various calculations, fields of intelligence, and computer science, such as networking, imaging, and other fields, such as biological sciences. In different applications, they present an appropriate construction means. There were limitations in the definition of fuzzy graphs (FGs), which prompted us to propose a new definition for IVFGs. Some interesting properties related to the new IVFGs are investigated, and enough conditions under which the level graph on IVFGs is equivalent are obtained. Therefore, in this study, we present the properties of a level graph (LG) of an IVFG, and four operations, the Cartesian product (CP), composition (CO), union, and join, are investigated on it. Today, in a treatment system, one of the issues that can be very valuable and important to the quality of service to patients is finding qualified and efficient people in each department, which is not an easy task. But the interval-valued fuzzy graph, as an important fuzzy graph, can help us by considering the ability of each person in the form of intervals of numbers and the effectiveness of each one on the other (according to the relationships between them) in order to find the most worthy people. So, an application of IVFG to find the most effective person in a hospital information system has been introduced.

This paper presents KM-SCR, a deductive-database system for automated geometry reasoning that aims to reduce redundant knowledge representation and inference overhead. First, a geometric-object merging mechanism consolidates collinear or coplanar objects and updates their associated relations, reducing redundant representations in the knowledge base. Second, a chain-of-equalities representation facilitates quantitative inference and supports algebraic reasoning through matrix-column compression and equation-system simplification. Third, semi-conditional rules divide rule-matching conditions into base conditions and remaining constraints, enabling staged candidate generation and constraint verification to reduce unnecessary matching operations. We establish the equivalence between semi-conditional rules and their original formulations at the rule-instance level and integrate the three mechanisms into an iterative reasoning workflow. Experiments on all 293 problems in FormalGeo7k-L6 show that KM-SCR solves 288 instances (98.29%), with a mean solving time of 4.06 s among successfully solved instances. On 40 sampled problems from each of levels L1–L5, the success rates range from 97.50% to 100.00%. Further analyses of theoretical inference space, actual rule instantiations, memory consumption, and solving time assess the effects of the proposed mechanisms on knowledge redundancy and inference efficiency.

Although Wu’s method has achieved remarkable success in automated geometric theorem proving, its proving process relies heavily on complex algebraic elimination operations, making it difficult to directly reveal the reasoning relationships between hypotheses and conclusions, thereby reducing the interpretability and readability of the resulting proofs. To address this issue, this paper presents a theoretical reconstruction of the proving mechanism of Wu’s method from the perspective of identity proofs. By establishing an identity representation between the conclusion polynomial and the hypothesis polynomials, the algebraic elimination process of Wu’s method is transformed into a structured proof representation with explicit logical semantics. To this end, a Remainder Tracking Matrix (RTM) is introduced, and a systematic method is designed for the joint construction of the characteristic sequence and its RTM during the ascending process, thereby providing a structured and traceable algebraic representation for the elimination procedure of Wu’s method. Furthermore, we realize a mechanized construction of identity proofs within Wu’s method, demonstrating its capability in constructing readable proofs. Additionally, we demonstrate the effectiveness and feasibility of the proposed approach via machine-assisted verification of several representative geometric theorems. This study offers a new pathway toward the structured representation of geometric proofs in Wu’s method and lays a theoretical foundation for the algebraic characterization of geometric invariants as well as for enhancing the explainability of automated geometric theorem proving.