A Method for Expanding Predicates and Rules in Automated Geometry Reasoning System

Abstract

Predicates and rules are usually enclosed as built-in functions in automated geometry reasoning systems, meaning users cannot add any predicate or rule, thus resulting in a limited reasoning capability of the systems. A method for expanding predicates and rules in automated geometry reasoning systems is, thus, proposed. Specifically, predicate and rule descriptions are transformed to knowledge trees and forests based on formal representations of geometric knowledge, and executable codes are dynamically and automatically generated by using “code templates”. Thus, a transformation from controlled natural language descriptions to mechanization algorithms is completed, and finally, the dynamic expansion of predicates and rules in the reasoning system is achieved. Moreover, the method has been implemented in an automated geometry reasoning system for Chinese college entrance examination questions, and the practicality and effectiveness of the method were tested. In conclusion, the enclosed setting, which is a shortcoming of traditional reasoning systems, is avoided, the user-defined dynamic expansion of predicates and rules is realized, the application scope of the reasoning system is extended, and the reasoning capability is improved.

Keywords

• mechanical geometry theorem proof
• mathematics mechanization
• forward chaining
• knowledge representation