Расширение предикатных формул линейными неравенствами и списками для спецификации программ

• Автор: Ашраф Абд Эль-Фаттах Мустафа Дарвиш
• Шифр специальности: 05.13.17
• Научная степень: Кандидатская
• Год защиты: 2006
• Место защиты: Санкт-Петербург
• Количество страниц: 232 с. : ил.

ОГЛАВЛЕНИЕ

Глава. Секвенциальное исчисление предикатов

1.1. Метаязык ДЛЯ определения логических формул

1.2. Определение пропозициональной формулы.

1.3. Формальный аппарат выводимости

1.4. Язык исчисления предикатов

1.5. Секвенциальное исчисление предикатов

Глава 2. Пропозициональное исчисление с неравенствами линейных комбинаций формул и принадлежностью значений таких комбинаций списку из них

2.1. Введение.

2.2. Определение пропозициональных формул,расширенных неравенствами линейных комбинаций и принадлежностью

значений спискам из них

2.3. Аксиомы и правила вывода предлагаемого исчисления
2.4.Теоремы о расширенном исчислении высказываний.
Глава 3. Расширенное исчисление предикатов первого порядка
3.1. Основные определения.
3.2. Исчисление для расширенных предикатных формул
3.3. Допустимость правила сечения.
3.4. Теоремы о свойствах исчисления.
Глава 4.Экспериментальная информационная система для образовательного процесса в Хелванском
университете Каир,Египет
4.1. Введение.
4.2. Информационная система для выбора бакалаврской
программы обучения.
4.3. Информационная система для выбора магистерской
программы обучения.
4.4. Информационная система для степени кандидата наук
РГШ на отделении математики
4.5. Информационная система для получения звания доцента
Глава 5. Формальный язык для проверки корректности
программ на основе расширенных предикатных формул
5.1. Введение и основные ПОНЯТИЯ
5.2. Определение языка спецификаций.
5.3. Синтаксис утверждения о корректности программы Ю
5.4. Аксиоматический подход к корректности программ
5.5. Примеры корректных программ с использование предложенного формального языка спецификаций в комментариях.
Заключение
Список литературы


Например, (0,5) и (7,) — интервалы двух вхождений слова «абра» в слово «абракадабра». Ь'), если а < а'. Интересно отметить, что существует взаимнооднозначное соответствие между множествами всех слов в алфавите {0,|} и множеством всех положительных натуральных чисел, задаваемое простым законом. Прежде всего все натуральные числа представляются словами а алфавите {0,1}. Всякому слову в алфавите {0,|} ставится в соответствие число в двоичной системе счисления: 1х где х отличается от х' заменой буквы | на букву 1. По этому закону словам Л,0,(0| соответствуют числа 1,, , 1, записанные в двоичной системе счисления. Слово в алфавите {1, 2, 3, 4, 5, 6, 7, 8, 9, X} можно интерпретировать как натуральное число, записанное по основанию в позиционной системе счисления с цифрами 1, 2, 3, 4, 5, 6, 7, 8, 9, (таким образом, число является цифрой Х). Пустое слово рассматривается как число 0. Определение пропозициональной формулы 1. Вначале необходимо определить пропозициональные переменные, которые по существу являются именами утверждений и могут принимать истинное или ложное значенис. В разных учебниках предлагаются различные способы задания пропозициональных переменных [,]. Далее для этой цели будем использовать идентификаторы, начинающиеся и заканчивающиеся пробелом, при этом первой буквой идентификатора является одна из букв р, ц, г, б. Это близко к использованию в языках программирования идентификаторов для булевых переменных. Здесь знак м означает пробел. Выражение ^(-,)означает вычеркивание пробела, расположенного рядом. Итак, пропозициональная переменная начинается и заканчивается одним пробелом (для краткости его часто будем опускать). Бинарная-логическая-связка: &; V; =>; <=>. Пусть X, У - Пропозициональная - формула, а — Бинарная-логическая связка. X, (Х&У), (XV У), (Х=> У), (Х<=> У) являются пропозициональными формулами. Примеры. V и)), (((и&л) =>р) =>л). Иногда используют кванторные пропозициональные формулы, имеющие определение. Квантор: V; 3. Пропозициональная — формула; Квантор Пропозициональная — переменная Кванторная—пропозициональная-формула. Обилие скобок, встречающееся в пропозициональных формулах, затрудняет восприятие последних. В связи с этим вводятся соглашения о сокращении скобок. Определяется следующий порядок старшинства (приоритета связывания) логических связок: конъюнкция старше дизъюнкции, которая, в свою очередь, старше импликации, последняя старше эквивалентности. Отношение старшинства является транзитивным, т. При этом из двух одинаковых логических связок, находящихся в формуле, старшей считается связка, стоящая левее. Скобки расставляются в выражении, которое просматривается слева направо (быть может, неоднократно). Более старшие логические связки заключаются в скобки с минимально возможными левыми и правыми частями формулы в первую очередь. При этом непосредственно после знака -1 и после пропозициональной переменной, стоящей сразу за квантором, левая скобка не вставляется. Пример. Scr. О & -'