Сводка определений и основных фактов (1157988), страница 6
Текст из файла (страница 6)
. Если Г – пустое множество, то
называется теоремой исчисления предикатов.
Теорема (Гёделя; корректности и полноты для исчисления предикатов): Формула является теоремой исчисления предикатов тогда и только тогда, когда она общезначима.
Следствие из первой теоремы Гёделя: Математика – неаксиоматизируемая наука.
4.2.
И
н
т
у
и
ц
и
о
н
и
с
т
с
к
а
я
л
о
г
и
к
а
Интуиционистская логика (логика Брауэра) – это классическая логика, из аксиом которой исключен закон «исключенного третьего».
Определение. Интуиционистская интерпретация – это тройка
, где
S – непустое множество альтернативных состояний (состояний знаний);
- отношение нестрогого частичного порядка, указывающее, что некоторое состояние знаний может быть достигнуто из другого и обладающее свойствами транзитивности, антисимметричности и рефлексивности; 
- оценка истинности (способность решать задачи в определенном состоянии).
Отношение выполнимости для интуиционистской логики будет выглядеть следующим образом:
Изменяется и понятие логического закона.
Определение. Формула
называется общезначимой с точки зрения интуиционистской логики (интуиционистски общезначимой, обозначается как 
), если формула
будет выполнима в любом состоянии S любой интерпретации
.
Утверждение. Если формула
интуиционистски общезначима, то она общезначима и с точки зрения классической логики предикатов.
Утверждение. Формулы и интуиционистски невыполнимы.
Замечание. Не существует ни одного содержательного математического утверждения, для которого нельзя было бы построить интуиционистского доказательства, однако все доказательства должны показывать правильность утверждения явно (конструктивно), поэтому все доказательства получаются более сложными, а результатом любого такого доказательства будет построение алгоритма.
Утверждение (дизъюнктивное свойство интуиционистской логики). Интуиционистская общезначимость формулы
эквивалентна интуиционистской общезначимости либо 
, либо
.
Утверждение. Формула
общезначима тогда и только тогда, когда существует такой терм t, что формула 
будет интуиционистски общезначимой.
4.3.
Л
о
г
и
к
а
Х
о
а
р
а
Пусть П – программа,
- отношение между ее входными и выходными данными (т.е. если при поступлении на вход значения х программа выдает у, то выражение 
является истинным).
Определение. Программа называется правильной, если на ее выходе всегда появляется результат, находящийся в определенном отношении с входными данными (т.е.
).
Определение. Тройкой Хоара называется формула вида {}
, где 
- формулы, а П – программа, причем если на входе программы П выполняется утверждение
, то на ее выходе выполняется отношение
. Формула
называется предусловием, формула
- постусловием.
Определение. Программа П называется частично корректной относительно предусловия
и постусловия , если общезначима формула {}
. Эту общезначимость следует понимать следующим образом: для любой допустимой интерпретации I и любого набора значений свободных переменных
из выполнимости формулы
(
) будет следовать, что после завершения программы П переменные примут значения , причем формула
будет выполнима на данных значениях переменных (
).
Определим модельный язык программирования:
П ::= (x = t)
| П1, П2
| if A then П1 else П2 fi
| while A do П1 od
| eps,
Где х – переменная, t – терм Пi – программы, А – атом, eps – пустота.
Определение. Правилом вывода называется фигура следующего вида:
, причем выражения в верхней части правила называются предпосылками, выражение в нижней части правила называется заключением. Семантика правила вывода такова: если истинным предпосылки, то истинно и заключения.
Рассмотрим следующую систему правил:
1.
(ослабления)
2.
(присваивания)
3.
(последовательного соединения)
4.
(ветвления)
5.
(итерации;
называется инвариантом оператора итерации, для проверки правильности работы цикла требуется его найти)
6. {}
(аксиома)
Система таких правил называется PVS (Prototype Verification System) и позволяет упрощать проверку правильности программ.
4.4. Логики знаний
Рассмотрим мультиагентную систему (сложную систему, принимающую решения) программ-агентов. При этом принятие решения может опираться на то, что знают или не знают другие участники процесса принятия решений.
Определение. Модальным оператором называется оператор
, который выражает отношение уверенности (необходимости). Его семантика такова: 
означает «я знаю, что формула
истинна».
Вопрос общезначимости формулы
- вопрос непротиворечивости базы знаний.
Вопрос общезначимости формулы
- вопрос полноты базы знаний.
4.5. Динамическая логика (логика программ)
| Программы - набор базовых действий (операторов) 1) - программа; 2) - программа; 3) - программа (|| - недетермированный выбор); 4) - программа; 5) - программа (тест; - формула). | Формулы - набор базовых условий (пропозиционных переменных) 1) - формула; 2) , , , - формулы; 3) если П – программа, то [] - формула. |
Синтаксис динамической логики состоит из двух частей:
Пример: выражение {
<if A then П1 else П2 fi >{
, записанное в терминах логики Хоара, в терминах динамической логики будет выглядеть как
.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
