Page 55 - 4868

53 Ошибка! Стиль не определен.

кожен з яких є аксіомою або може бути отриманий з попередніх рядків
шляхом застосування до них правила виведення.
Теорема – це будь-який рядок в доведенні. Таким чином, теореми або є
аксіомами, або отримані за допомогою застосування правил виведення до
інших теорем.
Сама по собі формальна логічна система є математичною абстракцією –
набором символів і відносин між ними. Логічна система стає цікавою, коли
формули являють собою твердження з деякої предметної області, а формули,
які є теоремами – це істинні твердження. Для цього потрібно забезпечити
інтерпретацію формули.
Інтерпретація логіки відображає кожну формулу в хибу або істину.
Логіка є несуперечливою щодо інтерпретації, якщо несуперечливі всі її
аксіоми і правила виведення. Аксіома несуперечлива, якщо вона
відображається в істину. Правило виведення несуперечливе, якщо його

наслідок відображається в істину, за умови, що всі його гіпотези
відображаються в істину. Отже, якщо логіка несуперечлива, то всі теореми є
істинними твердженнями в розглянутій області. У такому випадку
інтерпретація називається моделлю логіки.
Поняття повноти дуально поняттю несуперечності. Логіка є повною
щодо інтерпретації, якщо формула, яка відображається в істину, є теоремою,
тобто в даній логіці доказова будь-яка (дійсна) формула. Таким чином, якщо
ФАКТИ – це множина істинних тверджень, що виражаються формулами
логіки, а ТЕОРЕМИ – множина теорем логіки, то несуперечність означає, що
ТЕОРЕМИ  ФАКТИ, а повнота – ФАКТИ  ТЕОРЕМИ. Повна і
несуперечлива логіка дозволяє довести всі її істинні твердження.

8.2. Логіка програмування

Отже, логіка програмування є формальною логічною системою, яка
дозволяє встановлювати і обґрунтовувати (доводити) властивості програм.
Як і в будь-якій формальній логічній системі, в ЛП визначені символи,
формули, аксіоми і правила виведення. Символи ЛП – це предикати, фігурні
дужки і оператори мови програмування. Формули в ЛП називаються
трійками. Вони мають наступний вигляд:

{ } { }P S Q
,
де предикати P іQ визначають відношення між значеннями змінних
програми, а S – оператор або список операторів.
Ціль логіки програмування полягає в тому, щоб забезпечити можливість
обґрунтовувати (доводити) властивості виконання програми. Отже,
інтерпретація трійки характеризує відношення між предикатами P таQ і
списком операторів S .
Трійка{ } { }P S Q істинна за умови, якщо виконання програми

починається в стані, що задовольняє P , завершується успішно і
результуючий стан задовольняє Q.