Стаття присвячена дослідженням з вбудовування парамодуляційних правил у метод елімінації моделей та вхідну резолюцію. Даються результати про коректність та повноту побудованих розширень.
Ключові слова: резолюція, парамодуляція, метод елімінації моделей.
The paper is devoted to the research on the building-in of paramodulation rules into the model elimination method and input resolution. The results about the soundness and completeness of the constructed extensions are given.
Key Words: resolution, paramodulation, model elimination method.
