|
Умолчание называется замкнутым тогда и только тогда, когда формулы a , pi,..., 3m, у не содержат свободных переменных. Свободные переменные умолчания считаются квантифицированными квантором всеобщности. Незамкнутое умолчание называется открытым. Оио представляет общую схему вывода. Его конкретизацией является замкнутое умолчание, полученное заменой всех свободных переменных открытого умолчания на константы языка логики предикатов первого порядка. Формально, теория с умолчаниями Д это пара: Д = < D, F >, (3-28) где D множество умолчаний, F множество замкнутых формул логики первого порядка (заметим, что в общем случае J31,..., (Зш не обязательно замкнутые формулы и не обязательно отличные от у). Заметим, что теория называется замкнутой тогда и только тогда, когда все умолчания из D замкнуты. Теория с умолчаниями Д = < D, F > подразумевает существование некоторого (нулевого или больше) числа выполнимых множеств формул (т.н. расширений), каждая из которых либо входит в множество F, либо выводится из него по правилам классической логики и/или логики умолчаний. Формально расширение теории Д определяется следующим образом. Пусть L язык логики первого порядка, X подмножество из L, Tht( X ) • множество замкнутых формул, общезначимо выводимых из X по правилам вывода классической логики: ThL( Х ) = {w w е L, w замкнута и X w ). (3.29) Пусть Д = < D, F > теория с умолчаниями, S с L. Через T(S) обозначим наименьшее подмножество множества L, удовлетворяющее следующим условиям: 1 ) F с T(S), 2)ThL(T(S))-r(S), |
р1 ,..., ргп обоснование умолчания; у следствие умолчания; М символ метаязыка. Интуитивно умолчания имеют следующий смысл: если мы верим в а и [31,..., Рш не противоречит всему, во что мы верим, то можно верить и в у. Система логики умолчаний представляется теорией с умолчаниями (или точнее: с правилами с умолчаниями), состоящей из некоторого множества особо выделенных формул и правил вывода. В ней содержатся формулы логики предикатов, представляющие основную информацию о системе, обрабатываемую в соответствии с имеющимися аксиомами. Содержатся также правила умолчаний, отражающие различные утверждения, касающиеся исключений. Для такой системы существует несколько (нуль или больше) множеств выводимых предположений. Эти множества представляют различные картины мира, которые можно представить, исходя из теории с умолчаниями. Умолчание называется замкнутым тогда и только тогда, когда формулы а, ($1,..., {Зш, у не содержат свободных переменных. Свободные переменные умолчания считаются квантифицированными квантором всеобщности. Незамкнутое умолчание называется открытым. Оно представляет общую схему вывода. Его конкретизацией является замкнутое умолчание, полученное заменой всех свободных переменных открытого умолчания на константы языка логики предикатов первого порядка. Формально, теория с умолчаниями А это пара: А = < Б , Б>, (2.3.) 79 где Б множество умолчаний, И множество замкнутых формул логики первого порядка (заметим, что в общем случае (Зт не обязательно замкнутые формулы и не обязательно отличные от у). Заметим, что теория называется замкнутой тогда и только тогда, когда все умолчания из О замкнуты. Теория с умолчаниями Д = < Э, Р > подразумевает существование некоторого (нулевого или больше) числа выполнимых множеств формул (т.н. расширений), каждая из которых либо входит в множество Р, либо выводится из него по правилам классической логики и/или логики умолчаний. Формально расширение теории А определяется следующим образом. Пусть Ь язык логики первого порядка, X подмножество из Ь, ТЬ1,( X ) множество замкнутых формул, общезначимо выводимых из X по правилам вывода классической логики: Тйь ( Х ) = {\у w e L ,w замкнута и X м/ }. (2.4) Пусть А = < О, Р > теория с умолчаниями, Б с Ь. Через ЦБ) обозначим наименьшее подмножество множества Т, удовлетворяющее следующим условиям: 1 ) Р с Г(8 ), 2 ) ТЬь (Г(в)) = Гф), 3) если а:Мр1’ "'Мрт е Д а е Г(в) 7 и 1 (31,..., (Зт ё Б, тоуе Г(Б). Множество формул Е с Ь называется расширением для А тогда и только тогда, когда Г(Е) = Е (т.е. Е неподвижная точка оператора Г). Заметим, что добавление к множеству формул Р новой формулы ф может привести к тому, что у получившейся в результате модифициро80 |