Диссертация (1149226), страница 7
Текст из файла (страница 7)
В табличных методах, как правило,используются секвенциальные исчисления (см. [5]).Первые версии табличных методов независимо друг от друга предложилив 1955 году Э. В. Бет [57] (см. также на русском [1]) и Я. Хинтикка [86].Предложенный Бетом метод на основе семантических таблиц (отсюда название«метод семантических таблиц») впоследствии был упрощен для классическойлогики первого порядка Р. Смаллианом [132].
Смаллиан назвал свой методметодом аналитических таблиц. Другие варианты табличных методов такжепредложили М. Фиттинг [72] и С. Кангер [11].Существуют и другие методы, которые изначально создавались илиразвивались независимо от табличных методов, но по существу могутрассматриваться как их разновидность. Метод гипертаблиц (англ.
«hypertableaux») — метод логического вывода, в котором объединены идеи методааналитических таблиц и метода гиперрезолюций [56]. Метод также можнорассматривать как вариант семантической резолюции [79].28В англоязычных статьях используется термин «tableaux methods».33В число табличных методов также включают (см. аргументацию в [79])метод таблиц со связями29 [58] и метод устранения моделей Д.
Лавленда30 [101].Табличные методы оказались хорошо приспособленными для логическоговывода в неклассических логиках, таких как дескрипционные и модальные логики[79]. Одним из недостатков большинства табличныхметодов являетсяиспользование глобальных переменных: подстановка вместо переменной в однойветви дерева поиска вывода затрагивает все остальные ветви. Это приводит кнеобходимости выполнять поиск с возвратом (англ.
«backtracking»). Однакосуществуют варианты метода, которые используют локальные переменные.Например,вгипертабличномметодеподстановкивместопеременныхзатрагивают только ту ветвь, в которой они применяются. Это позволяетиспользовать алгоритм унификации и стратегию поглощения, как в методерезолюций.Из работ [132, 79, 98, 84] можно почерпнуть много информации поописанным здесь, а также по некоторым более редким табличным методам.Множество примеров доказательств методом аналитических таблиц (дляразличных логик, классических и неклассических) приведено в книге [118].1.5.4. Обратный метод МасловаОбратный метод и его модификацииОбратныйметодбылпредложенсоветскимматематикомСергеемЮрьевичем Масловым в 1964 году [21].
В первоначальном варианте метод былпредназначен для доказательства замкнутых предваренных формул классическойлогики первого порядка (без функциональных символов) следующего вида:(1.1)29Здесь приведен буквальный перевод англоязычного названия метода «connection tableaux».
Врусскоязычных источниках автор не встречал упоминаний этого метода.30Англоязычное название метода — «model elimination method».34В формуле (1.1)— кванторы (или),это множество всех переменных, входящих в формулу, а символы—обозначаютдизъюнкты (т.
е. дизъюнкции атомарных формул и их отрицаний).Предложенный С. Ю. Масловым метод опирался на использование теоремыЭрбрана и метода метапеременных (другими словами, локальных переменных)Н. А. Шанина. По сравнению с существовавшими на то время методами,использовавшими теорему Эрбрана, предложенный метод строил логическийвывод в противоположном направлении — не «снизу вверх», а «сверху вниз», т. е.от аксиом к целевой формуле. В связи с этим он и получил название «обратного».В качестве основного преимущества перед другими методами С.
Ю. Масловуказал, что обратный метод существенно использует особенности доказываемойформулы для построения экономного вывода.Впоследствии идеи обратного метода получили развитие в виде общейсхемы, применимой к различным секвенциальным исчислениям генценовскоготипа, обладающим свойством подформульности. В монографии [22, с. 27]С. Ю. Маслов пишет:«В дальнейшем выяснилось, что идеи, лежащие в основе обратного метода,по существу не связаны с теоремой Эрбрана для предваренных формул и могутбыть применены не только для случая произвольных формул классическогоисчисления предикатов, но и для других исчислений (исчисление предикатов сравенством, конструктивное исчисление)».Отметим, что свойство подформульности (в вывод формулы могут входитьтолько ее подформулы) выполняется для многих существующих логическихисчислений.
Это свойство использовалось еще Г. Генценом для доказательстваразрешимости интуиционистского исчисления высказываний (см. [5]).К идее общей схемы обратного метода С. Ю. Маслов пришел постепенно. Вранних работах С. Ю. Маслов совершенствовал свой метод и рассматривал егоприложения к теории разрешимых классов (свойство разрешимости заключаетсяв возможности определить для любой формулы из заданного класса, выводимаона или нет). Уже в работе [21] обратный метод был использован для35доказательстваразрешимостиодногоизклассовформул,названноговпоследствии классом Маслова по фамилии его первооткрывателя. В публикации[25] идеи С.
Ю. Маслова получили развитие в виде универсального способадоказательства разрешимости большинства известных на то время разрешимыхклассов формул классической логики первого порядка (до этого использовалосьнесколько разных методов доказательства). В работе [23] было предложенорасширение метода на произвольные формулы логики первого порядка сфункциональными символами, а также приведено доказательство разрешимостиодного класса формул. Дальнейшее развитие теоретические приложенияобратного метода получили в работах [22, 36, 26, 162, 140, 37].
Обратный методустановления выводимости стал темой докторской диссертации С. Ю. Маслова.Одной из наиболее важных работ С. Ю. Маслова, посвященных обратномуметоду, стала монография [22]. В ней автор предложил общую схему обратногометода, обобщив его на произвольные секвенциальные исчисления без правиласечения,обладающиесвойствомподформульности.Вуказаннойработеприводится несколько примеров классических исчислений обратного метода,рассматриваются особенности алгоритмов поиска вывода и разрешающихалгоритмов, которые можно создать на основе обратного метода. Напомним, чтоалгоритм поиска вывода получает на вход формулу, в случае ее выводимостигарантированно завершает работу и возвращает доказательство формулы (еслиформула невыводима, алгоритм может не завершить работу). Разрешающийалгоритм для любой формулы из заданного класса гарантированно завершаетработу и выдает ответ «да» или «нет», в зависимости от выводимости формулы.В большинстве работ С.
Ю. Маслова по обратному методу используютсяспециальные термины: «набор», «разбивка», «система зависимостей» и т. д. Приэтом понятия набора и системы зависимостей позволяют получить более сильныеварианты понятий «подстановка» и «унификация», широко используемыхавторами современных работ в области АЛВ.
Так, подстановка используется впонятиях подформульности и поднабора. Подобная связь между понятиямипрослеживаема, но не всегда сразу очевидна.36В работе С. Ю. Маслова и Г. Е. Минца [31] изложена более простаяформулировка одной из модификаций обратного метода для предваренныхформуллогикипервогопорядка.Приводитсядоказательствополнотыпредложенной модификации и полученное с помощью обратного методадоказательство разрешимости формул вида, гденаходится в КНФ. Встатье С. Ю. Маслова и В. П. Оревкова [26] этот класс формул называетсяклассом, а в статье Г. Е. Минца [108] — классом E. В книге [30], изданнойпосле трагической гибели в автокатастрофе Сергея Юрьевича Маслова, приведенаальтернативная формулировка той же модификации метода, только в терминах Fнаборов и подстановок.
В [30] отмечено, что при построении нового набораможно унифицировать подстановки наборов-посылок аналогично вычислениюнаиболее общего унификатора, однако сама процедура унификации несколькихподстановок не приведена31. Англоязычная статья Г. Е. Минца [108], близкая посодержанию к работе [31], содержит еще одну формулировку этой модификацииметодаскраткимдоказательствомполноты,атакжедоказательстворазрешимости класса E.Другой способ формулировки обратного метода в виде исчисленияпредикатов с унификацией32 предложил А. А.
Воронков в 1985 году, см. болеедоступную публикацию 1990 года [153].Первая формулировка обратного метода для логики первого порядка сравенствомпредставленавработеС. Ю. Маслова[27].Первая«резолютивноподобная»33 формулировка метода для этой же логики в видеисчисления с унификацией дана в статье А. Дегтярева [67].
Предлагаемый в этойработе подход заключается в устранении предиката равенства (и неравенства) изнаборов и последующем применении обратного метода к полученным наборам.31Для случая двух подстановок такая процедура приводится в [68].32В статье [68] используется термин «free-variable calculus».33Здесь используется перевод термина «resolution-like», предложенного в статье [68]. Данный терминозначает, что правила вывода исчисления имеют сходство с правилом резолюции.37Первые конкретизации общей схемы обратного метода для неклассическихлогиксформулировалГ.
Е. Минц[33]подназванием«резолютивныхисчислений». Обратному методу для интуиционистской логики первого порядкапосвящены работы [109, 139, 106]. Существуют модификации обратного метода идля других логик. Например, для многозначных логик обратный методсформулирован в [95].В. А. Лившиц в [100] предложил «резолютивноподобные» классическиеисчисления обратного метода для логики высказываний и логики первогопорядка. Статья также содержит важный исторический обзор работ по обратномуметоду.Дляклассическоймодификацийобратногологикиметода.существуетИзложениедостаточноидейбольшоеобратногочислометодаприменительно к логике высказываний и модификацию обратного метода дляэтой логики можно найти в статье С.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
