Предположение об уникальности имён

В логике первого порядка предположение об уникальности имён формализуется через предикат равенства (неравенства). Для любых различных констант ${\displaystyle c}$ и ${\displaystyle c'}$ вводится аксиома ${\displaystyle c\neq c'}$ (что эквивалентно ${\displaystyle \neg (c=c')}$). Для более сложных термов аксиоматика включает:^[1]

• ${\displaystyle f(X_{1},\dots ,X_{n})\neq g(Y_{1},\dots ,Y_{m})}$ для различных функциональных символов ${\displaystyle f}$ и ${\displaystyle g}$^[1];
• ${\displaystyle f(X_{1},\dots ,X_{n})\neq f(Y_{1},\dots ,Y_{n})\leftarrow X_{i}\neq Y_{i}}$^[1];
• ${\displaystyle f(X_{1},\dots ,X_{n})\neq c}$ для функции ${\displaystyle f}$ и константы ${\displaystyle c}$^[1].

Введение UNA строго ограничивает множество допустимых интерпретаций: из рассмотрения исключаются любые интерпретации, в которых функция интерпретации отображает разные константы или основные термы в один и тот же элемент домена^[1].

Предположение об уникальности имён тесно связано с другими логическими допущениями, применяемыми в системах представления знаний:

• Предположение об открытом мире (OWA): то, что неизвестно как истинное, считается неизвестным. Системы, основанные на OWA, по умолчанию не включают UNA, однако это допущение может быть добавлено в них вручную^[2].
• Предположение о закрытом мире (CWA): то, что неизвестно как истинное, считается ложным. Системы, использующие CWA, по умолчанию включают UNA^[2].

Предположение об уникальности имён по-разному применяется в различных системах и областях.

Считать предположение об уникальности имён выполняющимся означает, например, следующее:

• если для некой сущности с именем «свинья» определено свойство «свинья розового цвета», это не даёт никакой информации о цвете поросяти, хотя в реальности эти слова — синонимы. Следовательно, на вопрос «поросёнок розовый?» ответ будет ложь: во-первых, не определено наличие сущности с именем «поросёнок» и информации о её цвете; во-вторых, было бы некорректно использовать разные имена для одного и того же объекта. Существование синонимов не предполагается — их необходимо явно определять, например как свойства (имя: «Свинья», синоним_1: «Поросёнок», синоним_2: «Sus scrofa domesticus» и т. д.), при этом уникальный идентификатор выбирается один;
• если в списке пассажиров авиарейса имя предъявившегося на регистрацию пассажира не обнаружено, даже если он использует другое, хотя и эквивалентное имя (например, на другом языке), и при условии корректности и полноты списка, то такой человек не считается одним из пассажиров;
• в списке авиапассажиров два пассажира не могут иметь одинаковый идентификатор (поэтому неправильно использовать лишь имя и фамилию как уникальные идентификаторы для бронирования авиабилета из-за частых случаев однофамильцев): не допускается определение двух или более сущностей с разными именами, если они тождественны.
• В системах логического вывода принятие UNA блокирует вывод о тождестве объектов: два разных имени не могут быть признаны одной и той же сущностью, и любые утверждения об их равенстве расцениваются как логическое противоречие^[1].
• При проверке числовых ограничений (например, максимальной кардинальности) или функциональных свойств UNA предотвращает нежелательное слияние индивидов. Например, если задано ограничение, что человек может состоять в браке не более чем с одним человеком, а в базе знаний указано, что Питер женат на Энн и на Мэри, система с UNA зафиксирует нарушение ограничений. В системах без UNA (например, в OWL) это не вызовет ошибки: логический выводчик автоматически отождествит Энн и Мэри, сделав вывод, что это один и тот же человек.

В OWL (Web Ontology Language), семантика которого базируется на дескриптивных логиках^[3], предположение об уникальности имён не подразумевается, но имеются специальные конструкции для явного задания тождественности или различия между сущностями.

Два следующих утверждения соответственно выражают тождественность или различие двух имён^[10][11]:

• owl:sameAs
• owl:differentFrom

Для массового задания различия индивидов и имитации допущения об уникальности имён в OWL предусмотрены дополнительные конструкции:

• owl:AllDifferent (в функциональном синтаксисе OWL 2 — DifferentIndividuals) — класс или аксиома, утверждающая, что все индивиды в заданном списке попарно различны;
• owl:distinctMembers — свойство, связывающее экземпляр owl:AllDifferent со списком различных индивидов;
• NegativeObjectPropertyAssertion — аксиома, утверждающая, что заданный индивид не связан с другим индивидом определённым объектным свойством.

Хотя использование owl:sameAs обычно рекомендуется для обеспечения тесной связанности между различными базами знаний, в литературе существуют критические замечания относительно злоупотребления этим свойством, поскольку оно нередко применяется в иных смыслах — таких как «похож на», «отображает» и др. Классическая логическая интерпретация тождества часто оказывается слишком строгой, так как сущности могут совпадать лишь в определённых контекстах^[12]. В качестве альтернатив предлагаются контекстуализированная семантика^[12] и использование предикатов (например, skos:closeMatch) для обозначения частичного совпадения или схожести^[13].

В OWL 2 свойство owl:sameAs по определению является симметричным и транзитивным, представляя собой отношение эквивалентности. Благодаря этому логический вывод работает в обе стороны, и для корректного связывания сущностей явное дублирование утверждения в обоих направлениях не требуется.