Основные понятия и методы теории формальных систем



Скачать 460.88 Kb.
страница1/11
Дата08.11.2012
Размер460.88 Kb.
ТипМетодические указания
  1   2   3   4   5   6   7   8   9   10   11
МИНИСТЕРСТВО ОБРАЗОВАНИЯ РОССИЙСКОЙ ФЕДЕРАЦИИ

НИЖЕГОРОДСКИЙ ГОСУДАРСТВЕННЫЙ ТЕХНИЧЕСКИЙ УНИВЕРСИТЕТ


Факультет информационных систем и технологий
Кафедра теории цепей и телекоммуникации

ОСНОВНЫЕ ПОНЯТИЯ И МЕТОДЫ

ТЕОРИИ ФОРМАЛЬНЫХ СИСТЕМ
Методические указания к изучению курса

"Дискретная математика" и решению задач

для студентов специальности 200900

Нижний Новгород 2000

Составитель А. В. Волохович
УДК 519.5(075.5)

Основные понятия и методы теории формальных систем: Метод. указания к изучению курса "Дискретная математика" и решению задач для студентов специальности 200900 / НГТУ; Сост.: А. В. Волохович. Нижний Новгород, 2000. 31 с.

Данные методические указания являются вспомогательным материалом для изучения курса "Дискретная математика" (раздел "Формальные системы") и предназначены для самостоятельной проработки при подготовке к практическим занятиям.



Редактор Е. В. Комарова

Подп. к печ.25.09.2000. Формат 6084.Бумага газетная. Печать офсетная.

Печ.л. 2,0. Уч.-изд. л. 1,9. Тираж Заказ




Нижегородский государственный технический университет.

Типография НГТУ. 603600, Н.Новгород, ул. Минина, 24.
 Нижегородский государственный

технический университет, 2000

Введение

Принцип резолюции – универсальный способ доказательства утверждений. Наиболее широкое применение он находит при доказательстве высказываний, сформулированных на языке исчисления высказываний (ИВ) и исчисления предикатов (ИП).

В данной разработке ИВ и ИП вводятся как конкретизация общего понятия формальной системы. Излагается ряд основных результатов этих теорий, вводится понятие логического следствия; устанавливается, что проблема выводимости утверждения из набора предпосылок сводится к доказательству невыполнимости (противоречивости) некоторой конъюнктивной нормальной формы (КНФ). Для доказательства противоречивости КНФ вводится и изучается процедура резолюции, включая некоторые ее модификации (линейную и семантическую резолюции).

Известно, что проблема противоречивости КНФ NР - полна. Согласно естественнонаучной гипотезе Р МР, полиномиальных решающих алгоритмов для нее не существует. Вместе с тем выделяются частные классы КНФ, для которых удается построить алгоритмы решения с полиномиальной верхней оценкой временной вычислительной сложности.

При написании данной разработки использованы литературные источники [1-4].


Понятие формальной системы



Формальная система (ФС) считается заданной, если определены следующие ее компоненты: 1) алфавит; 2) совокупность правильно построенных формул; 3) множество аксиом; 4) множество правил вывода.

Алфавит ФС включает конечное или бесконечное число символов. Эти символы делятся на три группы – буквы, символы операций и связок, вспомогательные символы (скобки различных видов, запятые и т.д.). Количество символов связок, символов операций и вспомогательных символов конечно, число букв может быть бесконечно за счет индексов, принимающих натуральные значения.

Любую конечную последовательность символов алфавита именуем формулой ФС. В совокупности формул ФС выделено множество правильно построенных формул (ППФ). Для ППФ задаются правила их конструирования и эффективная процедура, позволяющая по каждой формуле ФС определить, является ли она ППФ.

Множество аксиом – это выделенное подмножество ППФ. Если множество аксиом бесконечно, то предполагается наличие процедуры проверки по ППФ, является ли она аксиомой.

Правила вывода позволяют из имеющегося множества ППФ (утверждений) получать новые ППФ – непосредственные следствия этих утверждений.

Последовательность ППФ А1, А2 , ..., Аn называется выводом в ФС, если для любого i=1,…,n ППA Аi является либо аксиомой AС, либо непосредственным следствием некоторых ППФ множества (A1, A2, …,Ai-1), получаемым применением к этим ППФ некоторого правила вывода; ППФ A называется теоремой ФС, если в данной ФС имеется вывод, в котором последней ППФ является A.

Формальная система называется разрешимой, если существует алгоритм определения по произвольной ППФ, является ли она теоремой. Если такого алгоритме не существует, то рассматриваемая ФС именуется неразрешимой.

Правильно построенная формула B выводима из совокупности ППФ (А1, А2 , ..., Аn), если существует последовательность ППФ В1 , В2 , ..., Вk такая, что Вk=В и для любого i=1,..,k формула Вi является либо аксиомой ФС, либо формулой множества (А1, А2 , ..., Аn), либо непосредственным следствием некоторых ППФ множества (В1 , В2 , ..., Вk), получаемых применением к этим ППФ одного из правил посылками или гипотезами. Формулы, выводимые из пустого множества посылок, являются теоремами.

Запись А1, А2 , ..., Аn |- В означает выводимость формулы В из множества посылок (А1, А2 , ..., Аn); запись |- В означает, что В является теоремой ФС. Если М={А1, А2 , ..., Аn}, то запись А1, А2 , ..., Аn |- В можно представить записью М |- В.

Очевидны следующие утверждения:

– если и , то ;

­– тогда и только тогда, когда в М имеется конечное подмножество M1 такое, что ;

– если и для любой формулы В из множества M1, .

Приведем простейший пример формальной системы. Считаем алфавит состоящим из символов |, = , +. Правила конструкции ППФ следующие:
1) | есть ППФ;

2) если а – ППФ, то а| также ППФ;

3) если а и b – ППФ, то а + b и а = b также ППФ;

4) других ППФ нет.

Система аксиом включает единственную аксиому: | = |. Единственное правило вывода следующее: из ППФ a = b выводится а + | = b |.

Очевидно, что теоремой в введенной ФС будет любая формула вида

|+|+|+…+|=|…|,
где слева и справа от знака = стоит одинаковое число символов |;

других теорем в ФС нет.

  1   2   3   4   5   6   7   8   9   10   11

Похожие:

Основные понятия и методы теории формальных систем icon{ моделирование систем } V1: { модуль Теоретические основы разработки математических моделей систем }
Современное состояние проблемы моделирования систем. Раздел Основные понятия теории моделирования систем }
Основные понятия и методы теории формальных систем iconВопросы вступительного экзамена по специальной дисциплине 08. 00. 13 Инструментальные методы экономики
Основные положения теории систем. Определение системы. Свойства системы. Классификация систем. Модели экономических систем
Основные понятия и методы теории формальных систем iconОсновные понятия теории множеств
Основные понятия теории множеств: Индивидуальные задания к модулю 1 / Юго-Зап гос ун-т; сост.: Т. В. Шевцова, Е. В. Скрипкина. Курск,...
Основные понятия и методы теории формальных систем iconТеория информационных процессов и систем. Курс лекций
Основные понятия и определения 7 Основные задачи теории информационных систе
Основные понятия и методы теории формальных систем iconТеория автоматов и формальных языков
Настоящий курс ставит своей целью ознакомление обучаемых с устройством теории формальных языков, а также с основными принципами,...
Основные понятия и методы теории формальных систем iconПрограмма дисциплины «Интеллектуальные агенты и агентные системы в электронном бизнесе»
Базовые понятия теории прикладных интеллекту-альных систем и теории многоагентных систем
Основные понятия и методы теории формальных систем iconУчебно-методический комплекс дисциплины теория систем и системный анализ Специальность
Системы и закономерности их функционирования и развития. Переходные процессы. Принцип обратной связи. Методы и модели теории систем....
Основные понятия и методы теории формальных систем iconГрафы 4 Основные понятия теории графов 4
Пример Метод модульно-ориентированного анализа и проектирования сложных систем 10
Основные понятия и методы теории формальных систем iconВопросы к экзамену Моделирование как метод научного познания. Модель и моделирование. Основные понятия
Общая схема процесса моделирования систем. Основные понятия процесса моделирования систем
Основные понятия и методы теории формальных систем iconЛекция №1. Предмет, язык и задачи общей теории систем
...
Разместите кнопку на своём сайте:
ru.convdocs.org


База данных защищена авторским правом ©ru.convdocs.org 2016
обратиться к администрации
ru.convdocs.org