Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску

Datalog - это язык программирования с декларативной логикой, который синтаксически является подмножеством Prolog . Он часто используется в качестве языка запросов для дедуктивных баз данных . В последние годы Datalog нашел новое применение в интеграции данных , извлечении информации , создании сетей , анализе программ , безопасности , облачных вычислениях и машинном обучении . [1] [2]

Его истоки восходят к началу логического программирования , но оно стало отдельной областью примерно в 1977 году, когда Эрве Галлер и Джек Минкер организовали семинар по логике и базам данных . [3] Дэвид Майер придумал термин Datalog. [4]

Функции, ограничения и расширения [ править ]

В отличие от Пролога, операторы программы Datalog могут быть изложены в любом порядке. Более того, запросы Datalog на конечных наборах гарантированно завершаются , поэтому Datalog не имеет оператора cut Prolog . Это делает Datalog полностью декларативным языком .

В отличие от Prolog, Datalog

  1. запрещает сложные термины в качестве аргументов предикатов , например, p (1, 2) допустим, но не p (f (1), 2),
  2. накладывает определенные ограничения стратификации на использование отрицания и рекурсии ,
  3. требует , чтобы каждая переменная , которая появляется в главе пункта также появляется в неарифметической положительный (т.е. не отрицается) буквального в теле статьи,
  4. требует, чтобы каждая переменная, появляющаяся в отрицательном литерале в теле предложения, также появлялась в некотором положительном литерале в теле предложения [5]

Оценка запроса с помощью Datalog основана на логике первого порядка и, следовательно, является надежной и полной . Однако Datalog не является полным по Тьюрингу и поэтому используется как предметно-ориентированный язык, который может использовать преимущества эффективных алгоритмов, разработанных для разрешения запросов. Действительно, были предложены различные методы для эффективного выполнения запросов, например, алгоритм Magic Sets, [6] табличное логическое программирование [7] или разрешение SLG. [8]

Некоторые широко используемые системы баз данных включают идеи и алгоритмы, разработанные для Datalog. Например, стандарт SQL: 1999 включает рекурсивные запросы , а алгоритм Magic Sets (первоначально разработанный для более быстрой оценки запросов журнала данных) реализован в IBM DB2 . [9] Более того, механизмы регистрации данных стоят за специализированными системами баз данных, такими как база данных Intellidimension для семантической сети . [ необходима цитата ]

В Datalog было сделано несколько расширений, например, для поддержки агрегатных функций , чтобы разрешить объектно-ориентированное программирование или разрешить дизъюнкции в качестве заголовков разделов . Эти расширения оказывают значительное влияние на определение семантики Datalog и реализацию соответствующего интерпретатора Datalog.

Фрагменты [ править ]

Программы регистрации данных могут использовать или не использовать отрицание в телах правил: программы регистрации данных с отрицанием часто должны использовать его как стратифицированное отрицание, чтобы гарантировать, что семантика четко определена. Программы регистрации данных могут использовать или не использовать неравенства между переменными в телах правил.

Были определены некоторые синтаксические фрагменты Datalog, например следующие (от наиболее ограниченных до наименее ограниченных):

  • линейный журнал данных , где тела правил должны состоять из одного атома
  • охраняемый журнал данных , где для каждого правила все переменные, которые встречаются в телах правил, должны встречаться вместе по крайней мере в одном атоме, называемом охранным атомом
  • пограничный журнал данных , где для каждого правила все переменные, которые совместно используются между телом правила и заголовком правила (называемые граничными переменными ), должны все вместе встречаться в охранном атоме.

Другое ограничение касается использования рекурсии: нерекурсивный журнал данных определяется запрещением рекурсии в определении программ журнала данных. Этот фрагмент журнала данных столь же выразителен, как объединение конъюнктивных запросов , но написание запросов в виде нерекурсивного журнала данных может быть более кратким.

Выразительность [ править ]

Проблема ограниченности для Datalog спрашивает для данной программы Datalog, является ли она ограниченной , т. Е. Максимальная глубина рекурсии, достигаемая при оценке программы во входной базе данных, может быть ограничена некоторой константой. Другими словами, этот вопрос спрашивает, можно ли переписать программу Datalog как нерекурсивную программу Datalog. Решение проблемы ограниченности на произвольных программах Datalog является неразрешимым , [10] , но это может быть сделано разрешимо путем ограничения некоторых фрагментов Datalog.

Пример [ править ]

Эти две строки определяют два факта , то есть вещи, которые всегда актуальны:

родитель ( Xerces ,  Brooke ). родитель ( ручей ,  дамокл ).

Вот что они имеют в виду: xerces - родитель ручья, а Brooke - родитель дамокла . Имена пишутся в нижнем регистре, потому что строки, начинающиеся с заглавной буквы, обозначают переменные.

Эти две строки определяют правила , которые определяют, как новые факты могут быть выведены из известных фактов.

предок ( X ,  Y )  : -  родитель ( X ,  Y ). ancestor ( X ,  Y )  : -  родитель ( X ,  Z ),  предок ( Z ,  Y ).

имея в виду:

  • X является предком Y, если X является предком Y.
  • X является предком Y, если X является родительским элементом некоторого Z, а Z является предком Y.

Эта строка представляет собой запрос:

? -  предок ( xerces ,  X ).

Он спрашивает следующее: Кто все X, предком которых является xerces? Он вернет ручей и дамокл, когда будет противопоставлен системе Datalog, содержащей факты и правила, описанные выше.

Подробнее о правилах: у правила есть : - символ посередине: часть слева от этого символа - это заголовок правила, часть справа - это тело . Правило читается так: <head> считается истинным, если известно, что <body> истинно . Заглавные буквы в правилах стоят для переменных: в данном примере, мы не знаем , кто X или Y является, но некоторый X является предком некоторого Y если X является родителем этого Y . Порядок предложений не имеет значения в Datalog, в отличие от Prolog, который зависит от порядка предложений для вычисления результата вызова запроса.

В журнале данных проводится различие между экстенсиональными предикатными символами (определяемыми фактами) и интенсиональными предикатными символами (определяемыми правилами). [11] В приведенном выше примере ancestor- это интенсиональный предикатный символ, который parentявляется экстенсиональным. Предикаты также могут быть определены фактами и правилами и поэтому не могут быть чисто экстенсиональными или интенсиональными, но любую программу Datalog можно переписать в эквивалентную программу без таких предикатных символов с повторяющимися ролями.

Синтаксис [ править ]

Программа Datalog состоит из списка фактов и правил ( Horn clauses ). [12] Если константа и переменная представляют собой два счетных набора констант и переменных соответственно, а отношение представляет собой счетный набор символов предиката , то следующая грамматика выражает структуру программы журнала данных:

< программа >  :: =  < факт >  < программа > | < правило >  < программа > | ɛ < факт >  :: =  < отношение > "(" < список-констант > ")." < правило >  :: =  < атом > ": -" < список атомов > "." < атом >  :: =  < отношение >"(" < список терминов >")" < список атомов >  :: =  < атом > | < атом > "," < список атомов > < термин >  :: =  < константа > | < переменная > < список-терминов >  :: =  < термин > | < термин > "," < список-терминов > < список-констант >  :: =  < константа >| < константа >"," < список констант >

Атомы также упоминаются в литературе как литералы .

Семантика [ править ]

Существует три широко используемых подхода к семантике программ Datalog: теоретико-модельный , фиксированный и теоретико-доказательный .

Теория моделей [ править ]

Факт или правило называется основанием, если все его подкатегории являются константами. Основное правило R 1 является основным экземпляром другого правила R 2, если R 1 является результатом подстановки констант для всех переменных в R 2 .

База Herbrand (см. Herbrand Universe ) программы Datalog - это набор всех основных атомов, которые могут быть созданы с помощью констант, указанных в программе. Интерпретация (также известная как экземпляр базы данных ) является подмножеством базы Эрбраны. Атом заземления истинна в интерпретации I , если оно является элементом I . Правило это верно в интерпретации I , если для каждого основного экземпляра этого правила, если все пункты в организме верно в I , то глава правила также верно в I .

Модель программы Datalog P является интерпретацией I из Р , который содержит все заземляющие факты P , и делает все правила P истинных в I . Теоретико-модельная семантика утверждает, что смысл программы Datalog - это ее минимальная модель (эквивалентно пересечение всех ее моделей). [13]

Семантика фиксированных точек [ править ]

Пусть I будет набором интерпретаций программы Datalog P (т.е. I = P ( H ), где H - база Эрбранда для P, а P - оператор powerset . Определите отображение от I до I следующим образом: Для каждого основного экземпляра каждое правило в P, если каждое предложение в теле находится во входной интерпретации, добавляем заголовок наземного экземпляра в выходную интерпретацию. Тогда неподвижной точкой этой карты является минимальная модель программы. Семантика фиксированной точки предлагает алгоритм для вычисления минимальной модели: начните с набора основных фактов в программе, затем несколько раз добавляйте следствия правил, пока не будет достигнута фиксированная точка. [14]

Оценка [ править ]

Есть много разных способов оценки программы Datalog с разными характеристиками.

Стратегии оценки снизу вверх [ править ]

Стратегии оценки снизу вверх начинаются с фактов в программе и многократно применяют правила до тех пор, пока не будет установлена ​​какая-то цель или запрос, или пока не будет создана полная минимальная модель программы.

Наивная оценка [ править ]

Наивная оценка отражает семантику фиксированных точек для программ Datalog . Наивная оценка использует набор «известных фактов», который инициализируется фактами в программе. Он продолжается путем повторного перечисления всех основных экземпляров каждого правила в программе. Если каждый атом в теле основного экземпляра входит в набор известных фактов, то головной атом добавляется к набору известных фактов. Этот процесс повторяется до тех пор, пока не будет достигнута фиксированная точка, и больше нельзя будет вывести факты. Наивная оценка дает полную минимальную модель программы. [15]

Системы, реализующие Datalog [ править ]

Вот краткий список систем, которые либо основаны на Datalog, либо предоставляют интерпретатор Datalog:

Бесплатное программное обеспечение / открытый исходный код [ править ]

Написано вИмяПопробуйте онлайнВнешняя база данныхОписаниеЛицензия
CXSBСистема логического программирования и дедуктивной базы данных для Unix и MS Windows с таблицами, обеспечивающими завершение и эффективность, как в Datalog, включая инкрементную оценку [16]GNU LGPL
C ++Коралл [17]Дедуктивная система баз данных, написанная на C ++ с полунаивной оценкой журнала данных. Разработан в 1988-1997 гг.индивидуальная лицензия, бесплатно для некоммерческого использования
DLV [18]Расширение Datalog, поддерживающее дизъюнктивные главные предложения.пользовательская лицензия, бесплатная для академического и некоммерческого образовательного использования, а также для использования некоммерческими организациями [19]
Inter4QL [20]интерпретатор командной строки с открытым исходным кодом для Datalog-подобного языка запросов 4QL, реализованный на C ++ для Windows, Mac OS X и Linux. Отрицание разрешено в заголовках и текстах правил, а также в рекурсии.GNU GPL v3
RDFox [21]RDF Triple Store с аргументацией Datalog. Реализует алгоритм FBF для инкрементальной оценки.пользовательская лицензия, бесплатно для некоммерческого использования [22]
Суфле [23]компилятор Datalog-to-C ++ с открытым исходным кодом, преобразующий Datalog в высокопроизводительный параллельный код C ++, специально разработанный для сложных запросов Datalog по большим наборам данных, например, встречающихся в контексте статического анализа программUPL v1.0
ClojureКаскалогHadoopбиблиотека Clojure для запроса данных, хранящихся в кластерах HadoopApache
Clojure Datalogдополнительная библиотека, реализующая аспекты DatalogОбщественная лицензия Eclipse 1.0
СутьдаАпач КафкаБаза данных общего назначения с «разукрупненной» архитектурой, использующая потоковую передачу документов и транзакций, ориентированную на журнал, для достижения значительной архитектурной гибкости и элегантного горизонтального масштабирования. Подключаемые компоненты включают Kafka, RocksDB и LMDB. По умолчанию индексы являются битемпоральными для поддержки запросов к журналу данных на определенный момент времени. Предоставляются Java и HTTP API.Лицензия MIT
Датаскриптв памятиНеизменяемая база данных и механизм запросов к журналу данных, который работает в браузереОбщественная лицензия Eclipse 1.0
ДаталевинLMDBФорк Datascript, оптимизированный для долговечного хранилища LMDB.Общественная лицензия Eclipse 1.0
Datahikeфайл, в памятиФорк Datascript с надежным бэкендом, использующий дерево автостопщиков .Общественная лицензия Eclipse 1.0
ErlangЖурнал данныхБиблиотека предназначена для запроса и формализации связи n-мерных потоков с помощью журнала данных. Он реализует специальный механизм запросов с использованием упрощенной версии общей парадигмы логического программирования . Библиотека облегчает разработку приложений для интеграции данных, обмена информацией и семантических веб-приложений.Apache v2
HaskellДина [24]Dyna - это декларативный язык программирования для статистического программирования ИИ. Язык основан на Datalog, поддерживает как прямую, так и обратную цепочку, а также инкрементную оценку.GNU AGPL v3
DDlog [25]DDlog - это инкрементный типизированный механизм регистрации данных в памяти. Он хорошо подходит для написания программ, которые постепенно обновляют свой вывод в ответ на изменения ввода. Программист DDlog декларативно определяет желаемое отображение ввода-вывода, используя диалект Datalog. Затем компилятор DDlog синтезирует эффективную инкрементную реализацию. DDlog основан на библиотеке дифференциального потока данных [26] .Лицензия MIT
ЯваAbcDatalog [27]AbcDatalog - это реализация с открытым исходным кодом языка логического программирования Datalog, написанного на Java. Он предоставляет готовые к использованию реализации общих алгоритмов оценки Datalog, а также некоторые экспериментальные многопоточные механизмы оценки. Он поддерживает языковые функции, выходящие за рамки основного Datalog, такие как явное (не) унификация терминов и стратифицированное отрицание. Кроме того, AbcDatalog спроектирован таким образом, чтобы его можно было легко расширять за счет новых механизмов оценки и новых языковых функций.BSD
ИРИС [28]IRIS расширяет Datalog с помощью функциональных символов, встроенных предикатов, локально стратифицированных или не стратифицированных логических программ (с использованием хорошо обоснованной семантики), небезопасных правил и типов данных схемы XML.GNU LGPL v2.1
Йенаструктура семантической паутины, которая включает реализацию журнала данных как часть механизма правил общего назначения, который обеспечивает поддержку OWL и RDFS . [29]Apache v2
SociaLite [30]SociaLite - это вариант журнала данных для крупномасштабного анализа графов, разработанный в Стэнфорде.Apache v2
Грааль [31]Graal - это набор инструментов Java, предназначенный для запросов к базам знаний в рамках экзистенциальных правил, также известных как Datalog +/-.CeCILL v2.1
FlixдаФункциональный и логический язык программирования, вдохновленный Datalog, расширенный определяемыми пользователем решетками и монотонными функциями фильтрации / передачи.Apache v2
LuaДаталог [32]Да [33]легкая дедуктивная система баз данных.GNU LGPL
OCamlжурнал данных [34]Реализация журнала данных в памяти для OCaml с алгоритмами восходящего и нисходящего типов.BSD, 2 предложения
ПрологDES [35]реализация с открытым исходным кодом, которая будет использоваться для обучения Datalog на курсахGNU LGPL
PythonpyDatalog11 диалектов SQLдобавляет логическое программирование в набор инструментов Python. Он может выполнять логические запросы к базам данных или объектам Python и использовать логические предложения для определения поведения классов Python.GNU LGPL
РакеткаКаталог данных Racket [36]GNU LGPL
Datafun [37]Обобщенный каталог данных по полурешеткам.GNU LGPL
Рубинцветение / бутонRuby DSL для программирования с использованием конструкций, ориентированных на данные, на основе расширения Dedalus для Datalog, которое добавляет к логике временное измерение.BSD 3-Clause
РжавчинаКрепCrepe - это библиотека, которая позволяет вам писать программы декларативной логики на Rust с синтаксисом, подобным Datalog. Он предоставляет процедурный макрос, который генерирует эффективный, безопасный код и легко взаимодействует с программами Rust. Он также поддерживает такие расширения, как стратифицированное отрицание, полунаивное вычисление и вызов внешних функций в правилах Datalog.Лицензия MIT / Apache 2.0
DatafrogDatafrog - это легкий движок Datalog, предназначенный для встраивания в другие программы Rust.Лицензия MIT / Apache 2.0
Tcltclbdd [38]Реализация на основе бинарных диаграмм решений . Создан для поддержки разработки оптимизирующего компилятора для Tcl.BSD
Другой или неизвестный языкbddbddb [39]реализация Datalog, выполненная в Стэнфордском университете . Он в основном используется для запроса байт-кода Java, включая анализ точек на большие программы Java.GNU LGPL
ConceptBase [40]дедуктивная и объектно-ориентированная система баз данных, основанная на оценщике запросов журнала данных: Пролог для инициируемых процедур и перезаписей, аксиоматизированный журнал данных под названием «Телос» для (мета) моделирования. В основном используется для концептуального моделирования и метамоделирования.BSD, параграф 2

Несвободное программное обеспечение [ править ]

  • Datomic - это распределенная база данных, предназначенная для обеспечения масштабируемых, гибких и интеллектуальных приложений, работающих на новых облачных архитектурах. В качестве языка запросов он использует Datalog.
  • FoundationDB предоставляет бесплатную привязку к базе данных для pyDatalog с руководством по его использованию. [41]
  • Leapsight Semantic Dataspace (LSD) - это распределенная дедуктивная база данных, которая обеспечивает высокую доступность, отказоустойчивость, простоту эксплуатации и масштабируемость. LSD использует Leaplog (реализация журнала данных) для запросов и рассуждений и был создан Leapsight. [42]
  • LogicBlox , коммерческая реализация Datalog , используемая для веб-приложений планирования розничной торговли и страхования.
  • Profium Sense - это собственная графовая база данных, совместимая с RDF, написанная на Java. Он обеспечивает поддержку оценки Datalog для определенных пользователем правил.
  • .QL , коммерческий объектно-ориентированный вариант Datalog, созданный Semmle для анализа исходного кода с целью обнаружения уязвимостей. [43]
  • SecPAL - язык политик безопасности, разработанный Microsoft Research . [44]
  • Stardog - это графическая база данных , реализованная на Java . Он обеспечивает поддержку RDF и всех профилей OWL 2, обеспечивая широкие возможности рассуждений, включая оценку журнала данных.
  • StrixDB: коммерческое хранилище графиков RDF, SPARQL, совместимое с Lua API и возможностями вывода данных. Может использоваться как модуль httpd ( Apache HTTP Server ) или как автономный (хотя бета-версии находятся под Perl Artistic License 2.0).

См. Также [ править ]

  • Программирование набора ответов
  • Конъюнктивный запрос
  • DLV
  • Flix
  • SWRL
  • Зависимость, генерирующая кортежи (TGD), язык ограничений целостности для реляционных баз данных с синтаксисом, аналогичным Datalog.

Ссылки [ править ]

  1. ^ Хуанг, Грин и Лу, «Журнал данных и новые приложения», SIGMOD 2011 (PDF) , Калифорнийский университет в Дэвисе.CS1 maint: несколько имен: список авторов ( ссылка ).
  2. ^ «Нейронный журнал данных во времени: информированное временное моделирование с помощью логической спецификации». Материалы ICML 2020 .
  3. ^ Галлер, Эрве; Минкер, Джон «Джек», ред. (1978), «Логика и базы данных, Симпозиум по логике и базам данных, Центр исследований и исследований в Тулузе, 1977», Успехи в теории баз данных , Нью-Йорк: Plenum Press, ISBN 978-0-306-40060-5.
  4. ^ Abiteboul, Serge ; Халл, Ричард; Виану, Виктор (1995), Основы баз данных , стр. 305, ISBN 9780201537710.
  5. ^ Даталог
  6. ^ Bancilhon. «Волшебные множества и другие странные способы реализации логических программ» (PDF) . ПТ : УНЛ. Архивировано из оригинального (PDF) 08 марта 2012 года. Цитировать журнал требует |journal=( помощь )
  7. ^ Пфеннинг, Франк; Schuermann, Карстен. «Руководство пользователя Twelf» . CMU. Цитировать журнал требует |journal=( помощь )
  8. ^ «Эффективное нисходящее вычисление запросов при хорошо обоснованной семантике» (PDF) . Цитировать журнал требует |journal=( помощь )
  9. ^ Грыз; Го; Лю; Зузарте (2004). «Выборка запросов в DB2 Universal Database» (PDF) . Материалы международной конференции ACM SIGMOD 2004 по управлению данными - SIGMOD '04 . п. 839. DOI : 10,1145 / 1007568,1007664 . ISBN  978-1581138597. S2CID  7775190 .
  10. ^ Хиллебранд, Герд G; Канеллакис, Пэрис С; Майерсон, Гарри Джи; Варди, Моше Y (1995-11-01). «Неразрешимые проблемы ограниченности для программ регистрации данных». Журнал логического программирования . 25 (2): 163–190. DOI : 10.1016 / 0743-1066 (95) 00051-K . ISSN 0743-1066 . 
  11. ^ Лифшиц (2011). «Программы регистрации данных и их стабильные модели». Даталог перезагружен . Конспект лекций по информатике. 6702 . ДЭ : Спрингер. С. 78–87. CiteSeerX 10.1.1.225.4027 . DOI : 10.1007 / 978-3-642-24206-9_5 . ISBN  978-3-642-24205-2.
  12. ^ Кери, Готтлоб & Tanca 1989 , стр. 146.
  13. ^ Кери, Готтлоб & Tanca 1989 , стр. 149.
  14. ^ Кери, Готтлоб & Tanca 1989 , стр. 150.
  15. ^ Кери, Готтлоб & Tanca 1989 , стр. 154.
  16. ^ Система XSB, версия 3.7.x, том 1: Руководство программиста (PDF) .
  17. ^ Веб-страница проекта базы данных кораллов.
  18. ^ "DLVSYSTEM Srl | DLV" . www.dlvsystem.com . Проверено 29 ноября 2018 ..
  19. ^ "DLVSYSTEM Srl | DLV" . www.dlvsystem.com . Проверено 29 ноября 2018 .
  20. ^ 4QL.
  21. ^ Веб-страница RDFox.
  22. ^ Лицензия RDFox , заархивировано из оригинала 21 февраля 2018 г. , получено 29 ноября 2018 г..
  23. ^ Компилятор Souffle , 12 декабря 2018 г..
  24. ^ "Dyna", веб-страница Dyna , заархивировано из оригинала 17 января 2016 года , получено 07 ноября 2016 года..
  25. ^ DDlog
  26. ^ Дифференциальный поток данных
  27. ^ AbcDatalog.
  28. ↑ Ирис рассуждающий.
  29. ^ "Йена" . Источник кузница .
  30. ^ Socialite домашнюю страницу , архивируются с оригинала на 2017-09-11 , извлекаться 2015-10-12.
  31. ^ Библиотека Грааля.
  32. ^ Рамсделл, "Даталог", Инструменты , NEU.
  33. ^ Сангкок, Y, "Wrapper", Mitre Datalog , Git hub, (скомпилировано в JavaScript).
  34. ^ Cruanes, Саймон, "журнал данных", журнал данных , GitHub.
  35. ^ Saenz-Perez (2011), "DES: дедуктивной системы баз данных", электронные примечания в теоретической информатике , ES , 271 : 63-78, DOI : 10.1016 / j.entcs.2011.02.011.
  36. ^ "Datalog", Racket (техническая документация).
  37. ^ "Datafun", Datafun in Racket (ссылки на статью, обсуждение и сайт github).
  38. Перейти ↑ Kenny, Kevin B (12–14 ноября 2014 г.). Диаграммы двоичных решений, реляционная алгебра и журнал данных: дедуктивные рассуждения для Tcl (PDF) . Двадцать первая ежегодная конференция Tcl / Tk. Портленд, штат Орегон . Проверено 29 декабря 2015 года . [ постоянная мертвая ссылка ]
  39. ^ "bddbddb", Source forge.
  40. ^ ConceptBase.
  41. ^ FoundationDB Datalog Tutorial , заархивировано из оригинала 09.08.2013..
  42. ^ «Прыжок» . Архивировано из оригинала на 2018-11-11.
  43. ^ Semmle QL.
  44. ^ "SecPAL" . Microsoft Research . Архивировано из оригинала на 2007-02-23.

Библиография [ править ]

  • Ceri, S .; Gottlob, G .; Танка, Л. (март 1989 г.). «Что вы всегда хотели знать о Datalog (и никогда не осмеливались спросить)» . IEEE Transactions по разработке знаний и данных . 1 (1): 146–166. CiteSeerX  10.1.1.210.1118 . DOI : 10.1109 / 69.43410 . ISSN  1041-4347 .

Дальнейшее чтение [ править ]

  • Грэдель, Эрих; Колайтис, Phokion G .; Либкин, Леонид ; Маартен, Маркс; Спенсер, Джоэл ; Варди, Моше Ю .; Венема, Иде; Вайнштейн, Скотт (2007), Теория конечных моделей и ее приложения , Тексты по теоретической информатике. Серия EATCS, Берлин: Springer-Verlag , ISBN 978-3-540-00428-8, Zbl  1133,03001