Введение в системы БД (542480), страница 237
Текст из файла (страница 237)
Дедуктивные аксиомы В этом подразделе объясняется уже упоминавшееся понятие дедуктивной аксиомы, которое также называется правилом вывода (нли правилом заключения). По своей сути дедуктивная аксиома — это правило, следуя которому на основе определенных фактов можно вывести новые факты. Например, на основе фактов "Аппе В бзе шог)зег ог" Вену" (" Анна — мать Бетти" ) и "Веку В г)зе гпогпег ог Сейа' ("Бетти — мать Селии" ) согласно очевидной дедуктивной аксиоме можно вывести, что "Аппе Ь г)зе Егапдшог)зег оТ Се))а" (" Анна — бабушка Селии" ).
Забегая наперед, можно представить дедуктивную СУБД, в которой два данных факта оформлены в виде кортежей отношения МОТНЕН ОР с атрибутами МОТНЕН (мать) и ОйООНТЕН (дочь). МОТНЕВ ОР Эти два факта будут основными аксиомами для системы. Предположим также, что дедуктивная аксиома формачьно определена в СУБД с использованием следующего гипотетического упрощенного синтаксиса. ТР МОТНЕН ОР ( Хю У ) йНО МОТНЕН ОР ( у, г ) ТНЕН ОййНОМОТНЕН ОР ( х, г ) ) Теперь это правило, выраженное в форме дедуктивной аксиомы, можно применить к данным, выраженным в форме основных аксиом (конкретные способы такого применения будут обсуждаться в разделе 23.4).
Это позволит получить результат бййНОМОТНЕЕ ОР(йппе, Се!Та). Таким образом, пользователи СУБД смогут создавать запросы наподобие "Кто является бабушкой Селии?" и "Кто является внучкой Анны?" (точнее будет спросить "Чьей бабушкой является Анна?" ). 901 Глава 23. Поеические системы управления базами данньп Сравним описанные идеи с традиционными концепциями баз данных.
Согласно традиционной терминологии дедуктивная аксиома может быть задана на основе приведенного ниже определения представления. ЧАВ 6КАНОМОТНЕК ОГ 71ЕН ( МХ.МОТНЕК АЕ 6КАНОМОТНЕВ, МХ.ОАООНТЕВ АН 6ВАНООАООНТЕВ) ННЕВЕ МХ.ОАО6НТЕК - "МХ.МОТНЕК Здесь умышленно используется стиль реляционного исчисления. МХ и МХ вЂ” переменные кортежа, которые изменяются на переменной-отношении МОТНЕВ ОГ. Запросы такого типа могут быть оформлены на основе следующего представления. 6Х.6ВАНОМОТНЕК ННЕКЕ 6Х.ОВАНООАООНТЕК = МАМЕ ( 'Се11а' ) 6Х.ОВАНООАООНТЕК ННЕКЕ 6Х.ОВАМОМОТНЕК = МАМЕ ( 'йппе' ) Здесь 6Х вЂ” переменная кортежа, изменяющаяся на переменной-отношении 6ВАНОМОТНЕК ОР. Таким образом, на основе другого синтаксиса и другой интерпретации был представлен материал, который в основном уже знаком читателю.
Однако в последующих разделах на нескольких более сложных примерах будет показано, что на самом деле различия между логическими системами и традиционными СУБД гораздо существеннее. 23.3. Исчисление высказываний В этом и следующем разделах кратко и весьма упрощенно описываются некоторые основные идеи логики.
Так, в данном разделе описывается исчисление высказываний (утверждений), а в следующем — исчисление предикатов (логических условий). Сразу же следует отметить, что описание исчисления высказываний приводится лишь для понимания более важной информации, изложенной ниже. Материал этих двух разделов является основой для остальных разделов данной главы. Исходя из предположения, что читатель знаком с основными понятиями булевой алгебры, в некоторых случаях мы будем использовать приведенные ниже термины и законы из этой области. ° Дистрибутивные законы Т АМО ( о ОВ А ) =- ( Т АНО о ) ОВ ( Т АКО А ) Т ОВ ( о АНО й ) м ( Т ОК д ) АНО ( Т ОК й ) ° ЗаконьчДв Моргана МОТ ( Т АМН о ) ж НОТ Т ОК НОТ о Нот ( Т ОВ о ) = Нот Т АНО Нот о Здесь Т, о и Ь вЂ” произвольные булевы выражения.
Сама по себе логика может быть определена как формальный метод рассуждений. В силу этого ее можно применять для выполнения таких формальных задач, как проверка допустимости аргумента, т.е. последовательная, шаг за шагом, проверка только структуры этого аргумента независимо от смысла шагов. В частности, благодаря такой формальности данный процесс может быть автоматизирован, т.е. запрограммирован и выполнен компьютером. 9Ог Часть )г. дополнительные аспекты Вообще говоря, исчисление высказываний и предикатов — это два специальных типа логических рассуждений (хотя на самом деле первый из них является подмножеством второго). Термин "исчисление", в свою очередь, служит всего лишь общим термином, используемым в любой системе с символическими вычислениями.
В нашем конкретном случае эти вычисления применяются для установления истинности значений некоторых формул нли выражений (т.е. истинны они или ложны). Термы Предположим для начала, что имеется набор объектов, называемых константами, о которых делаются различного рода утверждения (илн заключения). Согласно языку, принятому в области баз данных, эти константы являются значениями из основных доменов, а утверждением может быть, например, такое условное выражение, как "3 > 2". Тогда термом мы будем называть утверждение, которое содержит такие константы и обладает следующими свойствами.
1. Утверждения либо не содержат логических связок (подробности приводятся ниже), либо заключены в скобки. 2. Утверждения однозначно оцениваются либо как истинные, либо как ложные. Например, утверждения "Поставщик с номером '51' находится в городе 'Ьопдоп'", "Поставщик с номером '52' находится в городе 'Бовдоп'" и "Поставщик с номером '51' поставляет деталь с номером 'Р1'" являются термами (в рассматриваемом примере они оцениваются соответственно как истинное, ложное и истинное).
И наоборот, утверждения "Поставщик с номером '51' поставляет некоторую деталь с номером р", где р — переменная, и "Поставщик с номером '55' когда-нибудь в будущем будет поставлять деталь с номером 'Р1'" не являются термами, поскольку их нельзя однозначно оценить как истинные или ложные. Формулы Формула исчисления высказываний или, в более общем смысле, исчисления предикотое используется в СУБД, помимо всего прочего, и для представления запросов. <Формула> <терм> | йОт <терм <терм> ййо <формула> <терм> Ой <формула> <терм> ~ <формула> < терм> <атомарная формула> ) ( <формула> ) Формулы вычисляются исходя из истинности значений входящих в них термов с использованием обычных таблиц истинности лля связок.
Здесь следует отметить некоторые важные особенности. 1. Параметр <атомарная формула> — это логическое выражение, которое не содержит связок и не заключено в скобки. 903 Глава 23. Логические системы управления базами данных 2. Символом "~" обозначается связка типа логической иипитаяии. По определению выражение Т ~ д логически эквивалентно выражению НОТ Т ОА д. Замечание. В главе 7 и других главах для этой связки использовалась конструкция "1Р ...
ТНЕН ...". 3. К связкам применяются обычные правила приоритета выполнения (НОТ, затем АНР, затем ОН, затем ~), что позволяет избежать многократного использования скобок. 4. Высказывание — это просто элемент типа <форнула>, как он определен выше. Термин "формула" употребляется просто для согласования с материалом следуюшего раздела. Правила вывода Правила вывода для исчисления высказываний имеют следуюший вид. ЬТ= д Здесь символом "р"' обозначена фраза "Всегда верно, что".
Обратите внимание, что такие символы необходимы для составления мелнОтпвержделий, т.е. утверждений об утверждениях. Ниже приведено несколько примеров правил вывода. 1. 'р ( 1 АНО д ) =~ т 2.еу=ь( ГОнд) 3. р ( ( Т ~ д ) АНО ( д ~ Л ) ) ~ ( Г =ь Л ) 4. Т ( Г АНО ( Т =ь д ) ) ~ д Замечание. Это чрезвычайно важное правило называется правилои отделения (шобцз ропепз). Неформально оно интерпретируется так: если Т истинно и из У следует д, то д также должно быть истинным.
Допустим, например, что каждый из приведенных ниже фактов является истинным. а) У меня нет денег. б) Если у меня нет денег, я должен мыть посуду. Исходя из этих фактов можно заключить, что истинны.и является и следуюший факт. в) Я должен мыть посуду. Вот еше примеры правил вывода.
5. 'Е ( Т =ь ( д ~ Л ) ) =ь ( ( Т АНО д ) =ь Л ) б, р ( ( Г ОН д ) АНО ( НОТ д ОН Л ) ) =ь ( Т ОН Л ) Замечание. Также очень важным является правило, которое называется правилом резолюции. Более подробно оно описывается ниже, а затем мы вернемся к нему в разделе 23.4. 904 Часть )г. Дополнительные аспекты Доказательства Теперь нам известно все, что необходимо для создания формальных доказательств в контексте исчисления высказываний. Задача доказательства состоит в определении, будет ли некоторая данная формула д, т.е. заключение, логическим следствием (выводом) некоторого набора формул Е1, 12,..., Тл, т.е. предпосылок. Ниже дано символическое представление доказательства.
11, Г2, ..., Гл '1- д Такая форма записи с использованием символа метаутверждения "~-" интерпретируется как "д следует из 11, 12,..., 1д". Подобный способ выполнения называется прямым формированием цепочки и заключается в последовательном применении правил вывода к предпосылкам, затем — к формулам, выведенным из этих предпосылок, затем — к формулам, выведенным из этих формул, и т.д. до тех пор, пока не будет выведено заключение.
Иначе говоря, процесс "последовательного связывания" состоит в переходе от предпосылок к заключению. Однако существует несколько вариантов этой основной схемы. 1. Принятие предпосылки. Если заключение д имеет вид р =э д, то р принимается как дополнителы~пя предпосылка, а д выводится из заданных предпосылок и предпосылки р. 2. Обратное формирование цепочки. Вместо доказательства утверждения р =э д доказывается его контрапозиция (утверждение, обратное противоположному), т.е. НОТ д ~ НОТ р.
3. Приведение к противоречию. Вместо доказательства прямого утверждения р ~ д полагают, что р и йОТ д являются истинными, и затем приходят к противоречию. 4. Резолюция. В этом методе вывода используется правило резолюции (п. б предылушего перечня). Методику использования правила резолюции следует рассмотреть подробнее, поскольку она широко применяется на практике и, в частности, обобщается для исчисления предикатов, в чем мы убедимся в разделе 23,4.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
