Что поддерживается в логике первого порядка, чего нет в логике описания?

При изучении логики описания (ДО) очень часто можно прочитать, что это фрагмент логики первого порядка (ЛОЛ), но трудно прочесть что-то явно о том, что исключено из ДО, что является частью ЛОЛ, что делает ДО (со всеми его диалектами АЛК, ШОИН и т.д...) разрешимым. Или, другими словами, не могли бы вы предоставить мне несколько примеров в FOL, которые не могут быть выражены через DL (и которые являются причиной полу/неразрешимости в FOL)?


owl description-logic first-order-logic
person user3590127    schedule 16.07.2014    source источник
comment
Это интересный вопрос, но он слишком широк для формата Stack Overflow (либо слишком много возможных ответов, либо хорошие ответы будут слишком длинными для этого формата). но я подозреваю, что в сети уже есть много ответов.   -  person Joshua Taylor    schedule 16.07.2014
comment
В качестве очень простого примера вы не можете делать большинство вещей, требующих более двух переменных в списках рассылки. Например, вы не можете описать класс людей, которым нравится кто-то, кому нравится кто-то другой, кому нравится изначальный человек, тогда как в FOL это легко сделать: ∀x.(C(X) ↔ ∃y.(лайки(x,y) ∧ ∃z.(нравится(y,z) ∧ нравится(z,x)))).   -  person Joshua Taylor    schedule 16.07.2014
comment
В качестве другого примера, вы обычно не можете выразить согласие свойств в списках рассылки. Вы не можете говорить о классе людей, у которых первоклассные учителя также являются их любимыми учителями, но в ЛЖ это легко: ∀x.(C(x) ↔ ∃z.(любимыйУчитель(x,z) ∧ firstGradeTeacherOf(x, з))).   -  person Joshua Taylor    schedule 16.07.2014
comment
Спасибо Джошуа, это хорошие примеры! Таким образом, кажется, что всякий раз, когда одна переменная связана и используется более чем в одном свойстве, в DL становится сложно...   -  person user3590127    schedule 17.07.2014
comment
Нет, это не точное описание. Посмотрите на аксиому Дитя ⊑ ∃имеетОтца ⊓ ∃имеетМать. Это соответствует формуле FOL ∀x.(Child(x) ↔ (∃y.hasFather(x,y) ∧ ∃y.hasMother(x,y))), в которой используется переменная x с несколькими свойствами.   -  person Joshua Taylor    schedule 17.07.2014
comment
Итак, в основном используется более 2 (связанных) переменных, что невозможно выразить в DL!?   -  person user3590127    schedule 17.07.2014
comment
Для старых конструкций DL это часто верно, но в DL можно делать вещи, требующие большего количества переменных. Например, если вы объявляете свойство транзитивным, то вы говорите ∀x,y,z.(p(x,y) ∧ p(y,z) → p(x,z)), и для этого требуется три. В OWL 2 вы также можете создавать цепочки подсвойств, что означает, по существу, ∀w,x,y,z.(p(w,x) ∧ q(x,y) ∧ r(y,z) → s(w, я)). Это также может потребовать более двух переменных. Это не так просто, сколько переменных требуется? И DL могут делать некоторые вещи, которые вы не можете делать в FOL, например переходное закрытие ролей.   -  person Joshua Taylor    schedule 17.07.2014

Ответы (2)


arrow_upward
5
arrow_downward

Следующие факты о логике описания тесно связаны с разрешимостью:

  1. (форма) свойства модели дерева — это свойство важно для табличных методов;
  2. встраиваемость в мультимодальные системы, которые, как известно, «надежно разрешимы»;
  3. встраиваемость в так называемые охраняемые фрагменты ВОЛС — см. ниже;
  4. вложимость в двухпеременные фрагменты ВОЛ — которые разрешимы;
  5. населенный пункт — см. ниже.

Некоторые из этих фактов являются синтаксическими, а некоторые — семантическими. Ниже приведены две интересные, связанные с разрешимостью и более или менее синтаксические характеристики логики описания:

Местоположение (из The Description Logic Handbook, 2-е издание, раздел 3.6):

Одна из основных причин, по которой выполнимость и подчинение во многих логиках описания являются разрешимыми, хотя и очень сложными, заключается в том, что большинство конструкторов понятий могут выражать только локальные свойства элемента 〈...〉 Интуитивно это подразумевает, что ограничение относительно x не будет «говорить» об элементах, которые произвольно удалены (относительно ролевых ссылок) от x. Это также означает, что в ALC и во многих логиках описания утверждение об отдельном элементе не может устанавливать удовлетворяющие ему свойства всей структуры. Однако не всякая логика описания удовлетворяет локальности.

Защищенный фрагмент (из The Description Logic Handbook, 2-е издание, раздел 4.2.3)

Защищенные фрагменты получаются из логики первого порядка, позволяя использовать количественные переменные только в том случае, если эти переменные защищены соответствующими атомами до того, как они будут использованы в теле формулы. Точнее, квантификаторы могут появляться только в форме
     ∃y(P(x,y) ∧ Φ(y))         или      ∀y(P(x,y) ⊃ Φ(y))               (First Guarded Fragment)
     ∃y(P(x,y) ∧ Φ(x,y))      или      ∀y(P(x,y) ⊃ Φ(x,y))            (Защищенный фрагмент)
для атомов P, векторы переменных x и y и (первые) формулы охраняемого фрагмента Φ со свободными переменными в y и x (соответственно y).

С этих точек зрения проанализируйте примеры из комментариев @JoshuaTaylor:

  • ∀x.(C(X) ↔ ∃y.(нравится(x,y) ∧ ∃z.(нравится(y,z) ∧ нравится(z,x))))
  • ∀x.(C(x) ↔ ∃z.(любимыйУчитель(x,z) ∧ первыйУчительИз(x,z)))

Причины, по которым DL предпочтительнее FOL для представления знаний, связаны не только с разрешимостью или вычислительной сложностью. Посмотрите на слайд под названием «FOL как язык семантической паутины?» в этой лекции.

person Stanislav Kralin    schedule 06.11.2017

arrow_upward
2
arrow_downward

Как показали Тьюринг и Черч, ЛП неразрешима, потому что не существует алгоритма для определения того, верна ли формула ЛП. Многие логики описания являются разрешимыми фрагментами логики первого порядка, однако некоторые логики описания имеют больше возможностей, чем ЛОЛ, и многие логики пространственного, временного и нечеткого описания также неразрешимы.

person Leslie Sikos    schedule 30.10.2017