Rules cannot be recursively applied because the current implementation only allows one variable mask (assigning syntax to variable concepts) to be applied to a rule at a time.
can be used to infer that 2 > 0 given 2 > 1 and 1 > 0 because it just needs to apply the rule once with _x_ assigned to 2 and _z_ assigned 0.
However, given 3 > 2 as well, 3 > 0 cannot be inferred due to the rule needing to be applied once with _x_ assigned to 3 and _z_ assigned to 0 and then again with _x_ assigned to 2 or some other combination.
There is also a performance problems with the current implementation to check existence. It basically brute forces the existential property by trying all known concepts. Instead, the existential property can be satisfied by matching it with an expression that is known to be true. This will prevent trying concepts that have no chance of satisfying the existential property
Rules cannot be recursively applied because the current implementation only allows one variable mask (assigning syntax to variable concepts) to be applied to a rule at a time.
So the rule
can be used to infer that
2 > 0given2 > 1and1 > 0because it just needs to apply the rule once with_x_assigned to2and_z_assigned0.However, given
3 > 2as well,3 > 0cannot be inferred due to the rule needing to be applied once with_x_assigned to3and_z_assigned to0and then again with_x_assigned to2or some other combination.There is also a performance problems with the current implementation to check existence. It basically brute forces the existential property by trying all known concepts. Instead, the existential property can be satisfied by matching it with an expression that is known to be true. This will prevent trying concepts that have no chance of satisfying the existential property