Унификация логики первого порядка - PullRequest
Новая
       60

Унификация логики первого порядка

0 голосов
/ 10 февраля 2019

У меня есть вопрос об упражнении FOL, в котором я должен доказать, возможно ли объединить два предложения и, в положительном случае, показать, как их объединить. 

1) f(g(a,X),g(Y,Y))=f(g(a,b),g(f(a),f(Z)))

2) f(cons(cons(a,b)))=f(cons(cons(a,nil))

Длясначала я понял процедуру, поэтому дал значение f (a) Z , а затем я использовал замену o = {Y / f(a)} чтобы получить два одинаковых предложения.

Для второго действительно я не понял, что такое семантика предложения и как я могу его объединить.

1 Ответ

0 голосов
/ 21 февраля 2019

Алгоритм объединения прост

  1. , если обе стороны являются константами (числа, строки, атомы и т. Д.), Результат объединяет его, это один и тот же
  2. , если одна сторонаявляется переменной, мы добавляем подстановку этой переменной другой стороной
  3. , если обе стороны являются функциями, она объединяет, если это одна и та же функция (одно и то же имя) и ту же четность (количество параметров), затем унифицироватьРекурсивные параметры.

С вашими примерами:

  • f (g (a, X), g (Y, Y)) = f (g (a, б), g (f (a), f (Z))) 3-й случай, та же функция (f) и та же арность (2).Таким образом, вы должны унифицировать параметры:

    • g (a, X) = g (a, b)
    • g (Y, Y) = G (f (a), f(Z))

g (a, X) объединяется с g (a, b), потому что это та же самая функция (g) и та же самая арность (2).a = a объединяет (случай 1), X = b объединяет (случай 2) с заменой {X / b}

G (Y, Y) объединяет с G (f (a), f (Z))потому что это та же функция (g), то же самое arity (2).тогда Y = f (a) => замещение {Y / f (a)} и Y = f (Z) => f (a) объединяется с F (Z) {Z / a}

Вв конце вы получите o = {X / b, Y / f (a), Z / a}

  • f (cons (cons (a, b))) = f (cons (cons (a), ноль)))

То же самое и здесь.Та же самая функция (f) та же самая арность (1).Объединить cons (cons (a, b)) = cons (cons (a, nil)) Те же функции (cons), то же самое arity (1).Unify cons (a, b) = cons (a, nil) Та же функция (cons), та же арность (2).Unify a = a (OK), b = nil => NO

Это не объединяет.

...