Содержание к диссертации
Введение
Гласн 1. Секвенциальное исчисление предикатов 14
1.1. Метаязык для определения логических формул 14
1.2. Определение пропозициональной формулы 18
1.3. Формальный аппарат выводимости 23
1.4. Язык исчисления предикатов 25
1.5. Секвенциальное исчисление предикатов 29
Глава 2. Пропозициональное исчисление с неравенствами линейных комбинаций формул и принадлежностью значений таких комбинаций списку из них 37
2.1. Введение 37
2.2. Определение пропозициональных формул,расширенных неравенствами линейных комбинаций и принадлежностью значений спискам из них 39
2.3. Аксиомы и правила вывода предлагаемого исчисления 40
2.4. Теоремы о расширенном исчислении высказываний 44
Глава 3. Расширенное исчисление предикатов первого порядка со
3,1. Основные определения 60
3.2. Исчисление для расширенных предикатных формул 65
3.3. Допустимость правила сечения 69
3.4. Теоремы о свойствах исчисления 72
Глава 4. Экспериментальная информационная система для образовательного процесса в Хелванском университете (Каир.Египет) 76
4.1. Введение 76
4.2. Информационная система для выбора бакалаврской программы обучения 77
4.3. Информационная система для выбора магистерской программы обучения 87
4.4. Информационная система для степени кандидата наук (Ph.D) на отделении математики 95
4.5. Информационная система для получения звания доцента 99
Глава 5. Формальный язык для проверки корректности программ на основе расширенных предикатных формул 101
5.1. Введение и основные понятия 101
5.2. Определение языка спецификаций ЮЗ
5.3. Синтаксис утверждения о корректности программы Ю8
5.4. Аксиоматический подход к корректности программ 112
5.5. Примеры корректных программ с использование
предложенного формального языка спецификаций
в комментариях 115
Заключение 123
Список литературы
- Определение пропозициональной формулы
- Определение пропозициональных формул,расширенных неравенствами линейных комбинаций и принадлежностью значений спискам из них
- Исчисление для расширенных предикатных формул
- Информационная система для выбора магистерской программы обучения
Введение к работе
Представление знаний является самым важным понятием, связанным с искусственным интеллектом, и имеет широкие приложения [32,33].
Для того чтобы преодолеть многие трудности в области разработки программного обеспечения (ПО) всё большее количество учёных обращается к символической логике, как средству описания программного продукта [20,31,38].
Основная цель этой диссертации заключается в том, чтобы расширить логику высказываний и предикатную логику первого порядка более мощными инструментами описания спецификаций систем и схем ПО, а также разработать на ее основе язык спецификации программ, достаточный для доказательства корректности целочисленных программ, написанных на языке Паскаль.
Задача создания формализованного языка для доказательств правильности программ являет собой сердце современной компьютерной науки.В диссертации представлена расширенная логика высказываний с дополнительными линейными неравенствами пропозициональных формул и принадлежностью значения линейной комбинации пропозициональных формул списку их значений. Также представлено секвенциальное исчисление, соответствующее такой логике.Предложенное в диссертации секвенциальное исчисление может быть использовано для представления знаний в информационных системах.Имеются приложения нейронных сетей в медицине ,например,[43].Предложенные в этой логике расширенные формулы также более удобны для описания реализации идеи перцептрона и других нейронных сетей [22,41,48].
Основополагающим инструментом исследователей искусственного интеллекта является представление знаний, которое сводится к задаче разработки формального языка, подходящего для спецификации компьютерных программ [33].В этой диссертации разработаны важные средства расширения предикатной логики первого порядка, как формального языка для описания свойств и отношений между объектами. Язык, который разработан, также может быть использован в расширенных математических формулах для написания спецификаций программ, использующих типы короткого целого числа, целого числа и длинного целого числа. Предлагаемый расширенный язык может использовать метрику Хэмминта,сохраняя линейный характер исходных предикатов в отличие от [47],где используется эвклидова метрика.
Мак Дермотт и другие [35] утверждали, что ключом к написанию успешной программы, основанной на знаниях, является выбор правильных инструментов представления знаний.Многие варианты применения искусственного интеллекта сводятся к использованию лишь конечных множеств рациональных чисел из конечной области определения.В этой работе разработано расширение логики высказываний и секвенциального исчисления для него. Использованы линейные неравенства, в которых рациональные числа используются как коэффициенты линейных комбинаций [6,29,30]. Переход от исчислений гильбертовского типа к секвенциальным прослеживается ,например,в [19].Так определённое исчисление в ряде случаев более удобно применять к анализу и созданию информационных систем,чем традиционную логику первого порядка. Имеются приложения в экономикелтапример, [46].
В этой работе представлена новая логическая связка, которая называется линейным неравенством. Эта связка удобна для построения экспертных систем на языке Пролог, использованного в [36].
Основываясь на этой логической связке, была разработана экспертная система образовательной направленности для университета Хельван (Каир, Египет), предназначенная для того, чтобы давать рекомендации на разных этапах учёбы в университете.
Задача проверки правильности компьютерной программы связана с доказательством корректности программы. Одной из весомых иллюстраций практищности этой диссертации является то, что разработан в ней формальный язык спецификаций для доказательства корректности программ [25,45]. Такие инструменты, как, например, Java Modeling Language (JML) [29],возникли, чтобы помочь разработчикам более формально определить поведение компонент в больших системах.1МЬ основывается на традиционной логике, но в предложенном языке спецификаций использована расширенная логика, достаточная, как показано на примерах,для доказательства правильности учебных программ, написанных на языке Паскаль[17].
Определение пропозициональной формулы
Вначале необходимо определить пропозициональные переменные, которые по существу являются именами утверждений и могут принимать истинное или ложное значение.В разных учебниках предлагаются различные способы задания пропозициональных переменных [18,39].Далее для этой цели будем использовать идентификаторы, начинающиеся и заканчивающиеся пробелом, при этом первой буквой идентификатора является одна из букв р, q, г, S.3TO близко к использованию в языках программирования идентификаторов для булевых переменных.
Пропозициональная- переменная: р ; „?„;„ г„ ;„$„; Пропозициональная—переменная J_,) Буква-или-цифра м .
Здесь знак означает пробел.Выражение J !) означает вычеркивание пробела, расположенного рядом. Итак, пропозициональная переменная начинается и заканчивается одним пробелом (для краткости его часто будем опускать). Бинарная—логическая-связка: &; v; = Пусть X, Y-Пропозициональная-формула, а —Бинарная—логическая связка.Тогда Пропозициональная—формула: И; Л; Пропозициональная-переменная -і X; (X a Y);
Более подробно определение пропозициональной формулы выглядит следующим образом: 1) пропозициональные переменные и логические константы являются пропозициональными формулами; 2) если X и Y — пропозициональные формулы, то выражения -X, (X&Y), (X v Y), (X= Y), (X«Y) являются пропозициональными формулами. IIpHMepbi.((p&q) = ((гол) УИ)), (((и&л) =?р) = л).
Иногда используют кванторные пропозициональные формулы, имеющие определение. Квантор: V; 3. Кванторная—пропозициональная—формула:
Пропозициональная—формула; Квантор Пропозициональная—переменная Кванторная—пропозициональная-формула.
Обилие скобок, встречающееся в пропозициональных формулах, затрудняет восприятие последних.В связи с этим вводятся соглашения о сокращении скобок.
Определяется следующий порядок старшинства (приоритета связывания) логических связок: конъюнкция старше дизъюнкции, которая, в свою очередь, старше импликации, последняя старше эквивалентности. Отношение старшинства является транзитивным, т.е. если с, старше с2 а с2 старше с3, то с, старше с3 .При этом из двух одинаковых логических связок, находящихся в формуле, старшей считается связка, стоящая левее. Скобки расставляются в выражении, которое просматривается слева направо (быть может, неоднократно). Более старшие логические связки заключаются в скобки с минимально возможными левыми и правыми частями формулы в первую очередь.При этом непосредственно после знака -і и после пропозициональной переменной, стоящей сразу за квантором, левая скобка не вставляется. Пример. Расставим скобки в выражении /?&- # = /"= р&г. В первую очередь в скобки заключаются выраженияp&- q,p&r, затем р&-,д= г и, наконец, все выражение:
Можно с самого начала определить понятие возможно сокращенной пропозициональной формулы, в которой некоторые скобки могут быть опущены (согласно приведенным соглашениям), а некоторые могут быть продублированы. Приведем определение, основанное на совместной рекурсии.
Начальная—формула:И;Л;Пропозициональная—переменная; -і Начальная-формула; (ВспФ). ВспФ: Начальная-формула: ВспФ & ВспФ; ВспФ v ВспФ; ВспФ = ВспФ; ВспФ « ВспФ. Возможно—сокращенная —пропозициональная формула: ВспФ.
Возникает вопрос, а нельзя ли во всех случаях обходиться без скобок? Оказывается, можно,для этого достаточно отказаться от инфиксных обозначений (т.е. обозначений, при которых логическая связка стоит между аргументами), а воспользоваться только префиксными обозначениями (т.е. обозначениями, когда связка стоит перед аргументами—как отрицание) или же только постфиксными обозначениями (когда связка стоит после аргумента — аналогично тому, как штрих, обозначающий взятие производной).В случае, когда применяются префиксные обозначения, говорят о польской записи, которую впервые ввел польский логик Я.Лукасевич и использовала школа, созданная им.
Определение пропозициональных формул,расширенных неравенствами линейных комбинаций и принадлежностью значений спискам из них
Определение: "Линейная комбинация строк" Если р р рк - строки, то линейная комбинация строк-это а1р1+а2рг+... + сскРк где ах,а2 ...,ак являются рациональными числами, а если они отрицательны, то они должны быть заключены в круглые скобки. Определение: "Пропозициональная формула: (формула исчисленя высказываний)" Формулы исчисления высказываний определены следующим образом: - все логические константы и пропозициональные переменные - если VuW— формулы исчисления высказывания, то таковыми являются -пГ и (V = W), (V&W), (V v W), (V = W).
Примеры; (Aj= A2) и (-.А=Ф(А2&А!)). Определение: "Расширенная пропозициональная формула" (і) истина (1),ложь ,(-1) пропозициональные переменные являются расширенными пропозициональными формулами, (ii) если а,р и 5 - расширенные пропозициональные формулы, и LpL2,...,Lt (к 2) —линейные комбинации расширенных пропозициональных формул, тогда (Lt=L2), (=[L,,...,Lk]), (L,e[L2 LJ), (Li L2UL, L1)i{a&J3)i(a P), (a о /7), - a,(avP) и (ifa then p else 8 fl) также расширенные пропозициональные формулы. Используется традиционное значение знаков =,є, , &, = , = , v, -і и сокращение НЦ .Д вместо (L,=L2)&...&(Lb]=Lk]). Для интерпретации формулы используется традиционная таблица истинности, где истина —зтої, а ложь—это-1.Когда используем линейную комбинацию, подраумеваем арифметическое сложение и умножение. Равенства и неравенства имеют традиционный арифметический смысл. Более точно, значения формул вычисляются на основе следующих равенств [(А&В)] = тт([А1[В]), [(AvB)] = mxi([A],[B]), Ы] = - [А], [{A= B)] = [(-nAvB)l [(А «- В)] = тт([А = В)],[В = А)], где квадратные скобки обозначают вычисление значения формулы, которая заключена в них. Это завершает определение семантики расширенной пропозициональной формулы. Введем аксиомы и правила предлагаемого исчисления. В этом разделе будем использовать рациональные числа для коэффициентов линейных комбинаций. Определение: "Секвенция" Секвенция — слово, которое начинается со знака секвенции -» и состоит из списка формул (членов секвенции) [28].
Интерпретация секвенции—дизъюнкция интерпретаций всех формул (членов секвенции). Интерпретацией секвенции, которая состоит только из одного знака секвенции, является -1 (ложь).
Определим, когда секвенция является аксиомой исчисления.Сначала удалим все формулы, которые включают бинарные логические связки, кванторы и вложенные неравенства.После этого построим систему линейных неравенств. Нечетное количество логического отрицания перед формулой заменяем единственным арифметическим отрицанием и четное количество отрицаний предварительно удаляем.Тогда меняем все неравенства вида (х у)па неравенства (уих) и все неравенства вида (х у) ,где х,у — линейные комбинации пропозициональных nepeMeHHbiXjHaCy х) (в них логическое отрицание заменено одноместным минусом). Наконец, имеем систему линейных неравенств из секвенции.
Секвенция является аксиомой тогда и только тогда,когда полученная система неразрешима в рациональных числах из множества {-1,1} .Например, секвенция - (0 , А)(0 -А) — аксиома предлагаемого исчисления, где А—пропозициональная переменная.
Далее будем использовать прписные буквы для формул, и Г для конечных списков формул.Исчисление имеет следующие правила: правило перестановки членов секвенции. правило для вложенных неравенств: Вложенные неравенства типа (L, L2),(L, L2) могут быть заменены на (if Ц L2 then 1 else -\fi\(if і, sl then 1 else -\fi) соответственно. правила отрицания в неравенствах - Г(Ь+В Ь,+А) - r(L+-,B L,+A) -frlYL+ A i+iB) Г(Ь+-іА Ц+В) r(L+A L,+-,B) ( -) - r(L+B L,+-iA) и аналогичные правила с заменой на ,а также правила снятия и навешивания двойных отрицаний в равенствах и принадлежностях. правила отрицания вне неравенств
Исчисление для расширенных предикатных формул
Будем использовать правила из главы 2 и следующие правила для кванторов внутри неравенства.Ниже [учесть результат замены терма Т (v ), ( V), э ), вместо всех свободных вхождений переменной х в расширенной формуле первого порядка А.Когда используем эту аббревиатуру, полагаем, что свободное вхождение переменной х в А не находится в области действия вхождений кванторов с такими переменными непосредственно после этих кванторов, что эти переменные встречаются также в Т. - Т(Ц + [А] т L)(Lt + VxA L) Г(11+У 1) -»Г( И;+ ) г(А+и; х) -+F(Li+3xA L) ( 3) - Y{L Lx + [AYT L)(L Lt+ 3xA) - Г(1 Ц+ЗхА) и те же правила для вместо -; .Также будем использовать правила для внешнего квантора. ±Ж (V), -ЭЫ -+TVxA - ГВхА
Правила для кванторов имеют ограничение:переменная у не входит свободно в заключение правил (3 ),(3 ),( V),( V)H (V). Определение вывода, вы водимой секвенции и выводимой формулы для нового исчисления такое же как на стр.23. Определение (і) Язык V называют расширением L ,если (a) алфафит и языка L входит в алфавите и языка V, (b) каждая теорема в L является теоремой L . (Іі) Будем говорить, что расширение И языка L консервативно, если строка алфавита L —теорема в V, тогда и только тогда, когда эта она есть теорема в L .
Теорема і.Предлогаемое секвенциальное исчисления —консервативное расширение секвенциального исчисления первого порядка с чистыми секвенциями.
Доказательство.Определим вложение расширенной предикатной логики в двузначную.Каждое бескванторное неравенство, содержащее только атомарные формулы, заменяется эквивалентной (достаточно сложной) булевой функцией от конечного множества попарно различных двузначных атомарных формул с теми же векторами аргументов, что и каждая исходная атомарная формула. Неравенство, равенство и принадлежность линейной комбинации списку линейных комбинаций атомарных формул (каждая из которых принимает значения из {-1,1}. Может быть описана таблицей, по которой легко построить задающую ее формулу двузначной логики, например, в конъюнктивной нормальной форме. Сложность записи такого неравенства бескванторной формулой и объясняет полезность формализма, вводимого в настоящей главе и в предыдущей главе.
Будем говорить, что любая формула входит в себя положительно, формула А входит в формулу -Л отрицательно,связки &,v не меняют знака вхождения формулы. Знак подформулы ф любой формулы / определяется путем умножения знаков наименьшей строго объемлющей ее подформулы у/ в / на знак фву/.
Например, в формулу -»-i((-i3 xA)v В), обозначенную символом ф, формула —і— С—13 xA)v В) входит положительно, формула -.((-.3 хА) v В), входит в ф отрицательно, формула (( ,3xA)vB) входит в ф положительно, формула ЗхА и формула В входят в ф положительно, формула ЗхЛ входит в ф отрицательно, формула Л входит в ф отрицательно.
При наличии кванторов в формулах неравенства их следует вынести, навесив в результате на все неравенство. При вынесении кванторов удобно переименовать переменную, связанную этим квантором, на новую. Если формула вида хА входит в некоторое элементарное слагаемое неравенства положительно, то выносится квантор ,если отрицательно — то квантор, двойственный 0 .Такое вынесение кванторов сохраняет истинность интерпретаций формул.
Для более подробного описания тождественно истинной секвенции можно ввести преобразование 5 , преобразующее секвенции и внешние предикатные формулы расширенной предикатной логики соответственно в секвенции и формулы классической двузначной логики.
Информационная система для выбора магистерской программы обучения
Опишем, как введенный язык спецификаций может быть использован в доказательствах правильности программ, имеющихся в учебнике [17].
Достаточно математику описать практическое применение. Таким применением будет спецификации блоков программы использующие исчисления предикатов.Расширенное исчисление предикатов,можно использовать, как точную нотацию для описания функций программных блоков.Построим точные спецификации функций программных блоков. Такие спецификации состоят из 2 условий.Первое называется предусловием. Оно описывает соотношение между переменными и параметрами, прежде чем программа выполнена.Второе условие называется постусловием. Оно описывает соотношения между переменными и параметрами, после того как программа будет выполнена [45].
Этот раздел описывает доказываемые свойства компьютерных программ,написанных на языке программирования (языке Паскаль) [17].В этом случае можно констатировать поведение программы как утверждение, которое можно или доказать,или опровергнуть,или никогда ни доказать ни опровергнуть.
Традиционным подходом практиков к проблеме правильности программы будет тестирование программ и устранение ошибок. Программа исследуется путем тестирования, для того чтобы проверить является ли она правильной. Если нет, т.е., если результат дает неверное решениедо нужно попытаться найти "сбой" (т.е., источник ошибки).Тогда она сможет быть отлажена, и окончательный новый вариант программы необходимо испытать повторно.Когда найдено, что программа поступает удовлетворительно для достаточно большого и содержательного числа входных данных, приводят к заключению, что программа отлажена.
Единственный путь быть совершенно уверенным в правильности программы посредством тестирования-это исполнение программы для всех входных данных.Более того, не всегда есть возможность предвидеть предполагаемые результаты программы для любого входного сигнала.Например,можно легко исследовать программу путем подстановки входных данных и вычисления соответствующего результата вручную, пробегая по программе, и после этого проверить, что 2 выхода совпадают. Но если мы пишем программу, для того чтобы вычислить от десятично го числа п, то с трудом можно проверить правильность результата, вычисляя вручную результат,соответствующий,входу п = 109.
Однако, мы не должны прийти к неправильному заключению, что в будущем формальные доказательства правильности сделают методы тестирования программ устарелыми или никуда не годными. Приведем некоторые причины.
1.Формальные доказательства можно провести только с формальными спецификациями. Но очень часто мы совершаем ошибку, в процессе перехода от неформального к формальному описанию задачи.
2. Формальные доказательства программы могут быть длинными и сложными и таким образом, они могут быть также ошибочны.
3. Необходимо слишком много математических предпосылок.
По моему мнению, тестирование и доказательство правильности программы будут комплементарными инструментами, полезными как инженерное средство программирования, так и для того, чтобы увеличить доверие программиста к результату работы программы.
Доказывая правильность программы, в точности как математическую теорему, допускаем представление, что программами будут формальные объекты (т.е., они имеют формально определенные синтаксис и семантику).
