Formalizing a Constraint Deductive Database Language Based on Hereditary Harrop Formulas with Negation