Правило резолюции

Позволяет из дизъюнктов:

Получить новый дизъюнкт:

– наиболее общий унификатор термов S и t, обеспечивает их равенство и означает, что все подстановки унификатора выполнены для всех атомов, входящих в дизъюнкты D₁ и D₂. Дизъюнкты D₁ и D₂ называются родителями дизъюнкта D. В дизъюнкте D отсутствует пара , при этом и пара является тавтологией (тождественно истинной) и может быть удалена из дальнейших вычислений и выполняет правило склейки. Правило склейки позволяет из дизъюнкта получить дизъюнкт , т.е. осуществляется склеивание одинаковых атомов, полученных после унифицирующей подстановки.

Дата добавления: 2014-01-05