The translator generates some axioms and derived variables that are not very
useful. For example, in the attached problem, with the current translator
version (translator and preprocessor output files attached), axiom variable "2"
is always true, since it has exactly one triggering rule, which sets it from 0
to 1 with an empty body. Quoting from "output":
begin_rule
0
2 1 0
end_rule
We could simplify this by getting rid of
* derived variables that are constants and
* derived variables that are equivalent to other facts
Once we've systematically got rid of derivation rules with an empty body, we can
also simplify the axiom evaluation code which currently has to special-case
axioms with empty bodies. If we compile empty bodies away, we can replace this
special-case code with an assertion that the body is not empty.
|