Page 66 - 6571

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

Будь-яка формальна логічна система складається з правил,
визначених у термінах наступних множин:

1) символів;
2) формул, побудованих з цих символів;
3) виділених формул, що називаються аксіомами;
4) правил виведення.

Формулами є правильно побудовані послідовності символів.
Аксіоми – це особливі формули, які апріорі передбачаються як

істинні. Правила виведення визначають, як отримати справжні
формули з аксіом та інших істинних формул. Правила виведення
мають наступний вигляд:
H 1 , H 2 , ..., H n
,
C
де H – гіпотеза, а C – висновок. Значення правила виведення
i
полягає в тому, що якщо всі гіпотези істинні, то і висновок істин-
ний. І гіпотези, і висновок є формулами або їх схематичним по-

данням.
Доведення у формальній логічній системі – це послідовність
рядків, кожен з яких є аксіомою або може бути отриманий з по-

передніх рядків шляхом застосування до них правила виведення.
Теорема – це будь-який рядок в доведенні. Таким чином, те-
ореми або є аксіомами, або отримані за допомогою застосування
правил виведення до інших теорем.

Сама по собі формальна логічна система є математичною аб-
стракцією – набором символів і відносин між ними. Логічна сис-
тема стає цікавою, коли формули являють собою твердження з

деякої предметної області, а формули, які є теоремами – це істин-
ні твердження. Для цього потрібно забезпечити інтерпретацію
формули.

Інтерпретація логіки відображає кожну формулу в хибу або
істину. Логіка є несуперечливою щодо інтерпретації, якщо несу-
перечливі всі її аксіоми і правила виведення. Аксіома несупереч-

лива, якщо вона відображається в істину. Правило виведення не-

65