On $SLDNF$-resolution in logic programming with negation

The paper is devoted to the logic programming with negation and with built-in predicates. General logic programs (logic programs with negation) and general goals (goals with negation) are considered. Modification of $SLDNF$-resolution for built-in predicates is introduced. The soundness of modified SLDNF-resolution is proved. $SLDNF$-resolution used in real systems (practical $SLDNF$-resolution) is considered and the soundness of practical $SLDNF$-resolution is proved.