A new method for testing decision procedures in modal and terminological logics