An Efficient Automated Geometry Reasoning Method via Knowledge Merging and Semi-Conditional Rules
- 1Institute of Computing Science and Technology, Guangzhou University, Guangzhou 510006, China
- 2Guangzhou University of Software, Guangzhou 510990, China
Abstract
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.
Related
- Efficient Reasoning via Constrained Optimization in Latent Space
- Automated, Efficient, and Model-Free Inference for Randomized Clinical Trials via Data-Driven Covariate Adjustment
- ReAPO: Retry-Aware Policy Optimization for Efficient Exploration in LLM Reasoning
- Inverse Reasoning Models for Efficient Post-Training and Verification from Answer-Only Data
- Local Anticoncentration for Gaussian Boson Sampling via Conditional Wishart Geometry
BibTeX
@article{zhou2026efficient,
title = {{An Efficient Automated Geometry Reasoning Method via Knowledge Merging and Semi-Conditional Rules}},
author = {Qixin Zhou and Siran Lei and Ying Wang and Hao Guan and Yongsheng Rao},
journal = {Mathematics},
year = {2026},
month = nov,
doi = {10.3390/math14214038},
url = {https://www.mdpi.com/2227-7390/14/21/4038},
note = {CC BY 4.0},
}
RIS
TY - JOUR
TI - An Efficient Automated Geometry Reasoning Method via Knowledge Merging and Semi-Conditional Rules
AU - Qixin Zhou
AU - Siran Lei
AU - Ying Wang
AU - Hao Guan
AU - Yongsheng Rao
PY - 2026
DA - 2026/11/04
JO - Mathematics
DO - 10.3390/math14214038
UR - https://www.mdpi.com/2227-7390/14/21/4038
AB - 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.
SN - 2227-7390
ER -