Изменения

Перейти к: навигация, поиск

Исчисление высказываний

4822 байта добавлено, 19:35, 12 января 2012
Нет описания правки
|definition=
''Высказывание'' - любая формула, порожденная данными грамматиками.
}}
 
==Вычисление значений высказываний==
<wikitex>Теперь попробуем научиться вычислять значение высказываний.
Зададим некоторое множество истинностных значений $V$ и функции
оценки $f_\&, f_\vee, f_\to: V \times V \to V$, и $f_\neg: V \to V$,
по функции на каждую из связок и на отрицание. Также зададим ''оценку''
переменных, функцию, сопоставляющую множеству переменных $P$ некоторого
высказывания $\alpha$ --- функцию $f_P: P \to V$.</wikitex>
 
{{Определение
|definition=<wikitex>Если дано некоторое высказывание $\alpha$, в котором используются пропозициональные
переменные $v_1 \dots v_n$, то ''оценку'' данного высказывания $|\alpha|$ мы определим
следующим рекурсивным образом.
 
Возьмем дерево разбора высказывания, и возьмем его корень. В зависимости от правила, по которому получен корень, результатом оценки мы назовем:
 
* пропозициональная переменная $v_i$: $f_P (v_i)$
* конъюнкция выражений $\alpha$ и $\beta$: $f_\& (|\alpha|,|\beta|)$
* дизъюнкция выражений $\alpha$ и $\beta$: $f_\vee (|\alpha|,|\beta|)$
* импликация выражений $\alpha$ и $\beta$: $f_\to (|\alpha|,|\beta|)$
* отрицание выражения $\alpha$: $f_\neg (|\alpha|)$
* во всех остальных случаях оценка выражения равна оценке потомка в дереве.</wikitex>
}}
 
{{Теорема
|statement=
Любое выражение оценивается по этому определению
|proof=
<wikitex>Докажем индукцией по длине формулы, $n$; это традиционный способ доказательств
различных фактов про выражения. Данное доказательство подходит для первого
варианта грамматики.
 
База: $n=1$. Анализ грамматики показывает, что такая строка может состоять только из имени пропозициональной переменной. Очевидно, что указанный способ оценки позволяет такую строку оценить всегда.
 
Переход: пусть $n\ge 1$ и для $n$ все доказано. Рассмотрим строку длины $n+1$.
В дереве разбора данной строки есть некоторый корень, рассмотрим его. Он может быть:
* термом --- при этом это не пропозициональная переменная, так как длина строки больше 1. Значит, это либо выражение в скобках --- тогда все доказано по предположению индукции, поскольку длина выражения в скобках --- $n-1$, либо отрицание. Тогда применение функции $f_\neg$ к оценке строки длины $n$ даст оценку выражения.
* импликацией, конъюнкцией или дизъюнкцией, при этом примененный вариант правила добавляет новые терминальные символы в строку. Значит, здесь дерево разбора разделит строку на две, причем длины строго меньшей, чем $n$. В этом случае очевидно, что значение выражения будет вычислено.
* выражением, импликацией, конъюнкцией или дизъюнкцией, при этом примененный вариант правила не добавляет новых терминальных символов. В этом случае, спустившись (возможно, несколько раз) вниз по дереву мы дойдем либо до терма, либо до вариантов правил для импликации, конъюнкции или дизъюнкции, добавляющих терминальные символы, и окажемся в условиях предыдущих пунктов.</wikitex>
}}
97
правок

Навигация