Составляющие формальной системы. Язык формальной теории. Синтаксис формального языка, отношение между формулой и подформулой, сложные и атомарные формулы (стр. 13 )

Атомарные формулы предполагаются не являющимися явно открытыми, т. е. не содержащими явных вхождений свободных переменных. Тогда общезначимость отрицания формулы и конъюнкции формул устанавливается соответственно следующим образом.

Общезначимость формул, содержащих временные (темпоральные) кванторы, устанавливается для кванторов постоянства в будущем G, постоянства в прошлом GH и квантора необходимости, соответственно.

Двойственные кванторы случайности в будущем, случайности в прошлом и возможности определяются через ранее определённые.

Аксиоматика логики с ветвящимся временем может быть построена на аксиоматике, как минимум, исчисления высказываний и дополнительно может включать какие-либо из следующих.

Для любой атомарной формулы γ и формулы α, подформулой которой не является γ верно . Одним из обобщающих аналогов логик ветвящегося времени, для которого также могут использоваться правила немонотонного вывода, являются логики, которые получили название семантик возможных миров.

Формула является общезначимой в модели, тогда и только тогда когда она общезначима в любой микромодели.

Формула является общезначимой в структуре (временной модели), тогда и только тогда когда она общезначима во всех микромоделях этой структуры (временной модели).

50.  Язык интервальной временной логики. Базовые отношения интервальной временной логики.

Интервальная временная логика описывает свойства и отношения временных интервалов, и предикатов заданных для этих интервалов. Множество всех возможных временных интервалов интервальной временной логики обозначим I. Введём следующие сокращения.

Рассмотрим свойство отношение непосредственного следования интервалов. Запись читается как: «интервал i непосредственно предшествует интервалу j». Другие отношения над интервалами могут быть определены следующим образом.

Отношение «строго до» (отношение опосредованного предшествования)

Отношение «нестрого до» (отношение предшествования).

Отношение включения интервалов.

Отношение строгого включения интервалов.

Отношение разъединённости.

51.  Аксиоматика темпоральных отношений интервальной временной логики.

Интервальная временная логика описывает свойства и отношения временных интервалов, и предикатов заданных для этих интервалов. Множество всех возможных временных интервалов интервальной временной логики обозначим I.

Аксиоматика интервальной временной логики основывается на аксиоматике исчисления с равенством. Следующие пять аксиом описывают свойства временных интервалов и отношения непосредственного предшествования.

Следующие формулы определяют свойства слабого и сильного отрицаний в

интервальной временной логике.

52.  Аксиомы однородности и дискретной вариативности в интервальной временной логике. Теоремы.

Интервальная временная логика описывает свойства и отношения временных интервалов, и предикатов заданных для этих интервалов. Множество всех возможных временных интервалов интервальной временной логики обозначим I.

Эта логика рассматривает так называемые однородные предикаты. Любой однородный предикат по интервально переменной , обозначенный формулой , удовлетворяет следующей аксиомной схеме однородности.

Также для любого однородного предиката выполняется свойство дискретной вариативности (изменчивости), задаваемое следующей аксиомной схемой.

Следует отметить, что сильное отрицание однородного предиката, в общем случае не является однородным предикатом по той же интервальной (временной) переменной, это означает, что понятие сильного отрицания является относительным и темпорально независимым от предиката, который оно отрицает.

Теоремы интервальной временной логики являются следующие формулы.

Для однородных по переменным предикатов также верны следующие теоремы.

53.  Семантическая связь модальных и многозначных логик. Таблицы истинности логических функций для трёхзначной и четырёхзначной логики.

Модальные логики. Кванторы, которые выражают в том или ином виде временную (темпоральную) семантику, а именно: необходимость, возможность, будущность (будущее), прошлое, известность, допустимость, вера – получили название модальных.

Многозначные логики. Многозначные логики используют три и более значений истинности. Для каждой многозначной логики можно определить разные наборы логических операций, поэтому могут существовать разные логики равной значности.

Трехзначная логика. Значения это логики семантически интерпретируются так: «необходимо ложно» (0), «проблематично» (1), «необходимо истинно» (2), что во временной семантике означает, что формула ложна во все моменты времени, формула истинна для определенного множества моментов времени ложна в остальные моменты времени, и – формула истинна во все моменты времени.

Таблица истинности для отрицания и модальных кванторов.

Таблица истинности конъюнкции.

Таблица истинности дизъюнкции.

Таблица истинности импликации.

Таблица истинности эквиваленции.

Четырехзначная логика.

Значения рассматриваемой четырехзначной логики называются «необходимо ложно», «случайно ложно», «случайно истинно», «необходимо истинно» (0,1,2,3), что семантически означает, что формула ложна во все моменты времени, формула ложна сейчас и истинна потом, что формула истинна сейчас и ложна потом, и – формула истинна во все моменты времени.

Таблицы истинности для отрицания и модальных кванторов.

Таблица истинности конъюнкции.

Таблица истинности дизъюнкции.

Таблица истинности импликации.

Таблица истинности эквиваленции.

54.  Немонотонный, полумонотонный и монотонный вывод. Семантика, свойства.

Логики умолчаний введены и развиты Рейтером для формализации рассуждений, являющихся лишь выполнимыми. При неполной информации мы вынуждены получать всего лишь правдоподобные предположительные заключения. Иногда мы считаем абсолютно общими правила, которые правильны в большинстве случаев, но допускают некие исключения.

Рассмотрим рассуждение: Киви – птица, т. е. получается, что киви летает. Однако не все птицы летают, но можно без особого разрешения заключить, что киви летает, если это не запрещено. Это рассуждение с умолчаниями.

Логики умолчаний позволяют формализовать такие рассуждения в виде правил вывода, называемых умолчаниями:

- смысл таков: если мы верим в α и если β выполнимо вместе со всем, во что мы верим, то можно верить и γ.

Итак, правило «птицы вообще летают» выразимо в виде:

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

В общем виде умолчание выглядит следующим образом: , где α – требование, β – обоснование, γ – следствие. Среди умолчаний выделяют нормальные и полунормальные как и среди теорий с умолчанием.

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