Symbolic Inference Based on Rule Instantiation
Yunhao Liu, Zongkui He, Shiying Liu · 2024
Symbolic computation, as a focal point of research in automated reasoning, has made significant strides in recent decades, particularly in solving polynomial equations systems. Several computer algebra systems have been developed to assist humans in advanced mathematics, physics, engineering, and other fields. Inference rules are often described in code, requiring proficiency in their specific syntax for editing, which poses a challenge for non-programmer users. This paper introduces a novel approach utilizing an expression tree-based matching algorithm. This method matches rule expressions with instance expressions in a human-like manner, identifying multiple sets of variable substitutions. It achieves expression-level rule design independent of programming, making it applicable directly for formula equivalence transformations and inequality scaling.