На головну

 І ТЕОРІЯ АЛГОРИТМІВ |  множинами |  ВІДНОСИНИ |  обчислення предикатів |  Зведення формул до пропозицій |  Правило резолюції для обчислення висловлювань |  Правила резолюції для обчислення предикатів |  Спростування методом резолюції |  K-значна логіка |  Повнота і замкнутість функцій k-значної логіки |

ФОРМАЛЬНІ СИСТЕМИ (ТЕОРІЇ)

  1.  I-е покоління систем рухомого зв'язку - аналогові системи
  2.  I. визначник ТА СИСТЕМИ
  3.  I. Створення радянської судової системи
  4.  II-е покоління систем рухомого зв'язку - цифрові системи
  5.  III. Системи звичайних диференціальних рівнянь.
  6.  III.1.1 Загальний опис банківської системи
  7.  IX. СИСТЕМИ ГРИ

2.8.1. Визначення формальної теорії

формальна теорія Т це:

1) Безліч A символів утворюють алфавіт;

2) Безліч F слів в алфавіті А які називаються

формулами;

3) Підмножина Аx формул (  ), Які називаються аксіомами;

4) Безліч R відносин на безлічі формул, які називаються правіламівивода.

Таким чином формальна теорія Т є четвірки < A, F , Ax ,R >.

Зазвичай для освіти символів А використовуються кінцеві безлічі.

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

безлічі А и F в сукупності визначають мова або сигнатуру формальної теорії.

безліч аксіом Аx може бути кінцевим або нескінченним. Нескінченна безліч аксіом задається за допомогою кінцевого безлічі схем аксіом и правил породження аксіом з схем аксіом.

Безліч правил виведення R зазвичай звичайно.

Факт виведення формули G безпосередньо з формул  за правилом виведення R записується в такий спосіб:

.

При цьому формули  називається посилками, а G - укладенням.

висновком формули G з формул  формальної теорії T називається послідовність формул  , В якій остання формула  , А будь-яка інша формула  - Або аксіома, або вихідна формула  , Або безпосередньо виводиться з попередніх формул.

Цей факт записується так:

G.

При цьому  називаються гіпотезами виведення.

якщо G, То формула G називається теоремою теорії, тобто формула виводиться з аксіом (без гіпотез).

інтерпретацією формальної теорії Т в області інтерпретації М називається функція  , Яка кожній формулі F формальної теорії Т однозначно зіставляє деяке змістовне висловлювання щодо об'єктів безлічі М. Інтерпретація I називається моделлю формальної теорії Т, Якщо все теореми цієї теорії виконуються в інтерпретації I.

Формула називається загальнозначущої (тавтологією) Якщо вона істина в будь-якій інтерпретації.

Формула називається суперечливою, якщо вона помилкова в будь-якій інтерпретації.

формальна теорія Т називається несуперечливої, якщо хоча б одна її теорема не є протиріччям.

Формальна теорія Т є повної (адекватної), Якщо кожному істинному висловом М відповідає теорема в теорії Т.

Якщо для безлічі М існує формальна повністю не суперечлива теорія Т, то М називається аксіоматізіруемим (формалізованих).

Система аксіом формально не суперечливою теорії Т називається незалежною, якщо жодна з аксіом не виводиться з інших за правилами виведення теорії Т.

Формальна теорія Т називається можливо розв'язати, якщо існує алгоритм, який для будь-якої формули теорії визначає, чи є ця формула теоремою теорії чи ні.

 



 ФОРМУЛИ логіки ВИСЛОВЛЮВАНЬ |  обчислення висловлювань
© um.co.ua - учбові матеріали та реферати