moving some generic methods for loading axioms into a test reasoner
the first basic test for tracing completeness when the initial closure
has been computed w.r.t. non-redundant rules.
improved documentation
a first-cut implementation of tracing with completing the closure w.r.t.
redundant rules + a basic test.