In many cases an automatic deduction system cannot find complete proofs for particular theorems, goals, or questions requiring deductive support. In some cases information needed to complete proofs is missing from the database. In other cases proces...