 | В этой статье используется разметка HTML . ( Февраль 2019 г. ) |
Логика транзакций - это расширение логики предикатов, которое четко и декларативно учитывает явление изменения состояния в логических программах и базах данных . Это расширение добавляет связки, специально разработанные для объединения простых действий в сложные транзакции и для обеспечения контроля над их выполнением. Логика имеет естественную теорию модели и здравую и полную теорию доказательства . В Transaction Logic есть предложение Hornподмножество, которое имеет как процедурную, так и декларативную семантику. Важные особенности логики включают гипотетические и зафиксированные обновления, динамические ограничения на выполнение транзакции, недетерминизм и массовые обновления. Таким образом, Transaction Logic может декларативно фиксировать ряд нелогических явлений, включая процедурные знания в искусственном интеллекте , активные базы данных и методы с побочными эффектами в объектных базах данных .
Сделка Логика была первоначально предложена в [1] по Энтони Боннер и Майкл Кифер , а затем более подробно описано в [2] и. [3] Наиболее полное описание приводится в [4]
В последующие годы Transaction Logic была расширена различными способами, включая параллелизм , [5] проверяемые аргументы , [6] частично определенные действия [7] и другие функции. [8] [9]
В 2013 году оригинальная статья по Transaction Logic [1] выиграла 20-летнюю премию Test of Time Award как самая влиятельная статья из материалов конференции ICLP 1993 за предыдущие 20 лет. [ необходима цитата ]
Примеры [ править ]
Раскраска графиков. Здесь tinsert обозначает элементарную операцию обновления транзакционной вставки . Связка ⊗ называется последовательным соединением .
colorNode <- // правильно раскрашиваем один узел узел (N) ⊗ ¬ цветной (N, _) ⊗ цвет (C) ⊗ ¬ (смежные (N, N2) ∧ цветные (N2, C)) Мишура (цветная (N, C)).colorGraph <- ¬uncoloredNodesLeft.colorGraph <- colorNode ⊗ colorGraph.
Укладка пирамид. Элементарное обновление tdelete представляет собой операцию удаления транзакции .
stack (N, X) <- N> 0 ⊗ переместить (Y, X) ⊗ stack (N-1, Y).стек (0, X).move (X, Y) <- pickup (X) ⊗ putdown (X, Y).pickup (X) <- clear (X) ⊗ на (X, Y) ⊗ ⊗ tdelete (на (X, Y)) ⊗ tinsert (очистить (Y)).putdown (X, Y) <- шире (Y, X) ⊗ clear (Y) ⊗ tinsert (на (X, Y)) ⊗ tdelete (очистить (Y)).
Гипотетическое исполнение. Здесь <> является модальный оператор возможности: Если оба действие1 и action2 возможно, выполнить действие1 . В противном случае, если только action2 возможно, а затем выполнить его.
выполнить <- <> действие1 ⊗ <> действие2 ⊗ действие1. выполнить <- ¬ <> действие1 ⊗ <> действие2 ⊗ действие2.
Обедающие философы. Здесь | является логическим соединением параллельного соединения логики параллельных транзакций. [5]
столоваяФилософы <- phil (1) | фил (2) | фил (3) | Фил (4).
Реализации [ править ]
Существует ряд реализаций логики транзакций. Оригинальная реализация доступна здесь . Реализация логики параллельных транзакций доступна здесь . Здесь доступна логика транзакций, дополненная таблингом . Реализация Transaction Logic также была включена как часть системы представления знаний и рассуждений Flora-2 . Все эти реализации имеют открытый исходный код .
Дополнительные статьи по Transaction Logic можно найти на сайте Flora-2 .
Ссылки [ править ]
- ^ а б А.Дж. Боннер и М. Кифер (1993), Программирование логики транзакций , Международная конференция по логическому программированию (ICLP), 1993.
- ^ AJ Боннер и М. Кифер (1994), Обзор логики транзакций , Теоретическая информатика, 133: 2, 1994.
- ^ AJ Боннер и М. Кифер (1998), Логическое программирование транзакций баз данных в логике для баз данных и информационных систем, Дж. Чомицки и Г. Сааке (ред.), Kluwer Academic Publ., 1998.
- ^ AJ Боннер и М. Кифер (1995), Программирование логики транзакций (или логика декларативных и процедурных знаний) . Технический отчет CSRI-323, ноябрь 1995 г., Институт компьютерных исследований, Университет Торонто.
- ^ а б А.Дж. Боннер и М. Кифер (1996), Параллелизм и коммуникация в логике транзакций , Joint Intl. Конференция и симпозиум по логическому программированию, Бонн, Германия, сентябрь 1996 г.
- ^ П. Фодор и М. Кифер (2011), Транзакционная логика с дефолтами и теориями аргументации . В технических сообщениях 27-й Международной конференции по логическому программированию (ICLP), июль 2011 г.
- ^ М. Резк и М. Кифер (2012), Логика транзакций с частично определенными действиями . Журнал семантики данных, август 2012, т. 1, вып. 2, Springer.
- ^ Х. Давулку, М. Кифер и И.В. Рамакришнан (2004), CTR-S: логика для определения контрактов в семантических веб-сервисах. Материалы 13-й конференции World Wide Web (WWW2004), май 2004 г.
- ^ П. Фодор и М. Кифер (2010), Таблинг для логики транзакций . В материалах 12-го международного симпозиума ACM SIGPLAN по принципам и практике декларативного программирования (PPDP), июль 2010 г.
