Implementation of a general completion procedure parameterized by built-in theories and strategies