Аксиома пустого оператора

Правило для пустого оператора утверждает, что оператор skip (пустой оператор) не меняет состояния программы, поэтому утверждение, верное до skip, остаётся верным после его выполнения.

Аксиома оператора присваивания

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

Здесь означает выражение P в котором все вхождениясвободной переменной x заменены выражением E.

Смысл аксиомы присваивания заключается в том, что истинность эквивалентна после выполнения присваивания. Таким образом, если имело значение «истина» до присваивания, согласно аксиоме присваивания будет иметь значение «истина» после присваивания. И наоборот, если было равно «ложь» до оператора присваивания, должно быть равно «ложь» после.

Примеры корректных троек:

Аксиома присваивания в формулировке Хоара не применима, когда более одного идентификатора ссылаются на одно и то же значение. Например,

является неверным утверждением, если x и y ссылаются на одну и ту же переменную, так как никакое предусловие не может обеспечить, чтобы y было равно 3 после того, как x присвоено 2.

Правило композиции

Правило композиции Хоара применяется к последовательному выполнению программ S и T, где S выполняется до T, что записывается как S;T.

Например, рассмотрим два экземпляра аксиомы присваивания:

Согласно правилу композиции, мы получаем:

Нечёткая логика (англ. fuzzylogic) и теория нечётких множеств — раздел математики, являющийся обобщением классической логики и теории множеств.

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

Есть два способа реализации дизъюнкции и конъюнкции:

#Максиминный подход:

a || b =>max(a, b)

a && b =>min(a, b)

#Колорометрический подход:

a || b => a + b - a * b

a && b => a * b

Отрицание задается единственным способом (не трудно догадаться):

!a => 1 - a

Легко проверить, что для крайних случаев — когда значения переменных исключительно 1 или 0 — приведенные выше функции дают таблицы истинности операций классической логики. Готово! Теперь у нас есть расширенная логика, обладающая невероятной мощью, простотой и при этом полностью совместимая с классической логикой в предельных случаях. Значит везде, где мы [программисты] используем логические выражения, мы можем использовать выражения нечеткой логики? Не совсем.

Дело в том, что все операторы языков программирования требуют четких условий, поэтому в какой-то момент всегда приходится из нечеткой степени истинности получать четкий критерий срабатывания. Это похоже на то, что происходит в квантовом мире: до тех пор, пока система эволюционирует в соответствии с уравнением Шредингера, ее квантовое состояние изменяется детерминированно и непрерывно, но как только мы прикасаемся к системе, происходит квантовый скачок, и система сваливается в одно из дискретных состояний. В нечеткой логике это называется дефаззификацией. Природа просто превращает квантовое состояние в вероятность и бросает кости, но вообще говоря методы дефаззификации бывают разные. Я не буду углубляться в эту тему, потому что объем ее тянет на отдельную статью. Упомяну лишь только, что метод дефаззификации следует выбирать, учитывая семантику задачи.

Для примера представим себе систему управления ракетой, использующую нечеткую логику для обхода препятствий. Представим себе, что ракета летит точно в гору, и система управления вычисляет решение: лететь вправо — 0.5, лететь влево — 0.5. Если использовать дефаззификацию методом центра масс, то система управления даст команду — лететь прямо. Бум! Очевидно, что в этом случае правильное решение — бросить кости и получить команду «влево» или «вправо» с вероятностью 50%.

В простейшем случае, когда нужно принять решение на основании степени истинности, можно разбить множество [0,1] на интервалы и использовать if-else-if.

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

Модальная (от лат. – способ, мера) логика — логика, в которой кроме стандартных логических связок, переменных и/или предикатов есть модальности (модальные операторы). Модальности бывают разные; наиболее распространенывременны́е («когда-то в будущем», «всегда в прошлом», «всегда» и т. д.) и пространственные («здесь», «где-то», «близко» и т. д.). Например, модальная логика способна оперировать утверждениями типа «Москва всегда была столицей России» или «Санкт-Петербург, когда-то в прошлом, был столицей России», которые невозможно или крайне сложно выразить в немодальном языке. Кроме временных и пространственных модальностей есть и другие, например «известно, что» (логика знания) или «можно доказать, что» (логика доказуемости).

Обычно для обозначения модального оператора используется и двойственный к нему :

Это отражает то, что сказать «Москва когда-то была столицей России» то же самое, что сказать «не верно, что Москва никогда не была столицей России».

· Логические

· L — необходимо

· M — возможно

· С — случайно

· Фактические

· — необходимо

· — возможно

· — случайно

· Деонтические(древнегр. deon, deontos — должное, необходимое) модальные понятия:

· обязательно

· разрешено

· запрещено

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