Active rules termination analysis based on enhanced formula of a triggering cycle

Current methods remain largely uncertain of rules termination decision. Some methods are based on a logical formula for a rule set, but only those non-updatable or finitely updatable variables can be contained in a formula. Some other methods are based on triggering and activation graphs, but they do not consider whether all rules of a triggering cycle can be executed infinitely within a single execution cycle. Most methods cannot conclude termination if a rule set contains only those cycles that can be executed a finite number of times. This paper explicates the concepts of activation path and the execution sequence of a triggering cycle and the method to construct a formula that is able to include updatable variables, many termination cases that cannot be determined by previous methods, can now be detected.