Тета-категоризация

Тета-подчинение (θ-подчинение или просто подчинённое) — это разрешимое отношение между двумя предложениями первого порядка , которое гарантирует, что одно предложение логически влечет другое. Впервые оно было введено Джоном Аланом Робинсоном в 1965 году и стало фундаментальным понятием в индуктивном логическом программировании . Решение вопроса о том, θ-подчиняет ли данное предложение другое, является NP-полной задачей.

Предложение, то есть дизъюнкция литералов первого порядка , можно рассматривать как множество, содержащее все его дизъюнкты.

При таком соглашении предложение θ-включает предложение, если существует замена , при которой предложение, полученное путем применения к, является подмножеством . ^[1]${\textstyle c_{1}}$${\textstyle c_{2}}$ ${\displaystyle \тета}$${\textstyle \тета}$${\textstyle c_{1}}$${\textstyle c_{2}}$

θ-подчинение — более слабое отношение, чем логическое следование , то есть всякий раз, когда предложение θ-подчиняет предложение , то логически влечет . Однако обратное неверно: предложение может логически влечь другое предложение, но не θ-подчинять его.${\textstyle c_{1}}$${\textstyle c_{2}}$${\textstyle c_{1}}$${\textstyle c_{2}}$

θ-подчинение разрешимо; точнее, проблема того, является ли одно предложение θ-подчинением другого, является NP-полной по длине предложений. Это по-прежнему верно при ограничении настройки парами предложений Хорна . ^[2]

Как бинарное отношение между предложениями Хорна, θ-подчинение является рефлексивным и транзитивным . Поэтому оно определяет предпорядок . Оно не является антисимметричным , поскольку различные предложения могут быть синтаксическими вариантами друг друга. Однако в каждом классе эквивалентности предложений, которые взаимно θ-подчиняют друг друга, существует уникальное кратчайшее предложение с точностью до переименования переменных, которое может быть эффективно вычислено. Класс частных относительно этого отношения эквивалентности представляет собой полную решетку , которая имеет как бесконечные восходящие, так и бесконечные нисходящие цепи. Подмножество этой решетки известно какГрафик уточнения .^[3]

θ-подчинение было впервые введено Дж. Аланом Робинсоном в 1965 году в контексте резолюции ^[4] и впервые применено к индуктивному логическому программированию Гордоном Плоткиным в 1970 году для поиска и сокращения наименьших общих обобщений множеств предложений. ^[5] В 1977 году Льюис Д. Бакстер доказывает, что θ-подчинение является NP-полным ^[6], а основополагающая работа 1979 года по NP-полным проблемам, Computers and Intractability , включает его в свой список NP-полных проблем. ^[2]

Доказательства теорем, основанные на исчислении резолюции или суперпозиции, используют θ-подчинение для удаления избыточных предложений. ^[7] Кроме того, θ-подчинение является наиболее известным понятием вывода, используемым в индуктивном логическом программировании , где оно является основным инструментом для определения того, является ли одно предложение специализацией или обобщением другого. ^[1] Оно также используется для проверки того, охватывает ли предложение пример, и для определения того, является ли данная пара предложений избыточной. ^[2]

• Бакстер, Льюис Денвер (сентябрь 1977 г.). Сложность объединения (PDF) (Диссертация). Университет Ватерлоо.
• Де Рэдт, Люк (2008), Логическое и реляционное обучение, Когнитивные технологии, Берлин, Гейдельберг: Springer, Bibcode : 2008lrl..book.....D, doi : 10.1007/978-3-540-68856-3, ISBN 978-3-540-20040-6
• Kietz, Jörg-Uwe; Lübbe, Marcus (1994), «Эффективный алгоритм подчинения для индуктивного логического программирования», Machine Learning Proceedings 1994 , Elsevier, стр.  130–138 , doi :10.1016/b978-1-55860-335-6.50024-6, ISBN 9781558603356, получено 2023-11-26
• Плоткин, Гордон Д. (1970). Автоматические методы индуктивного вывода (PDF) (PhD). Эдинбургский университет. hdl :1842/6656.
• Робинсон, JA (1965). «Машинно-ориентированная логика, основанная на принципе разрешения». Журнал ACM . 12 (1): 23– 41. doi : 10.1145/321250.321253 . S2CID  14389185.
• Вальдманн, Уве; Турре, Софи; Робиллард, Саймон; Бланшетт, Жасмин (ноябрь 2022 г.). «Комплексная структура доказательства теоремы о насыщении». Журнал автоматизированного рассуждения . 66 (4): 499– 539. doi :10.1007/s10817-022-09621-7. ISSN  0168-7433. PMC 9637109.  PMID 36353684  .