Для применения резолюции необходимо найти два дизъюнкта, содержащие литералы с противоположными знаками: F(tl,..,tn) и ØF(tl,..,tn). Необходимо, чтобы совпадали не только имена предикатов, но и их аргументы. Напомним, что аргументы предиката это термы: константы, переменные и функции (сложные имена).
С константами уже ничего сделать нельзя, а вот вместо переменных можно подставить любые термы, используя правило:
х Р(х) É Р(а) (если предикат истинен для всех х, то он истинен и для конкретного значения переменной).
При этом надо делать такую подстановку, чтобы литералы полностью совпали.
Нам важно ваше мнение! Был ли полезен опубликованный материал? Да | Нет
studopedia.su - Студопедия (2013 - 2024) год. Все материалы представленные на сайте исключительно с целью ознакомления читателями и не преследуют коммерческих целей или нарушение авторских прав!Последнее добавление