A recent paper [1] laid out the theoretical basis for effective reasoning with infinite stable models and normal programs with function symbols. For the class of finitary programs introduced there, ground queries are decidable and nonground queries are semi-decidable under both credulous and skeptical stable model semantics. Finitary programs are expressive enough to simulate any given Turing machine. In order to exploit the potential expressiveness of finitary programs, a family of tools is needed, including: