On $SLDNF$-resolution in logic programming with negation

Работа посвящена логическому программированию с отрицанием и встроенными предикатами. Рассматриваются обобщенные логические программы (логические программы, использующие отрицание) и обобщенные запросы (запросы, использующие отрицание). Предложена модификация $SLDNF$-резолюции для встроенных предикатов. Доказана логическая непротиворечивость модифицированной $SLDNF$-резолюции. Рассмотрена $SLDNF$-резолюция, используемая в реальных системах логического программирования (практическая $SLDNF$-резолюция) и доказана ее непротиворечивость.