На головну

система Генцен

  1.  I. Хто є хто, або система цінностей
  2.  I. Поняття, предмет, система виконавчого провадження
  3.  II. Система дієслівних форм. Основи дієслова.
  4.  II. Система основних понять кризової психології
  5.  Kell-система
  6.  MRP і DRP відносяться до систем виштовхує типу.
  7.  Name System (DNS - доменна система імен).

В її основі лежить поняття секвенції.

Секвенції мають вигляд

антецедент - A1, A2... An ?? B1, B2, ... Bn - сукцедент

знак секвенції

Змістовно це рівносильно висловом:

A1 & A2& ... & An ® B1U B2U ... U Bn

аксіома (схема аксіом) В системі Генцен єдина і вона має вигляд:

A?? A

Правила виведення:

(З секвенций над рисою виведені секвенції під рискою, а Г позначає якесь безліч формул).

1) A, Г?? В 1) ? Г?? A; Г?? А® В

Г?? А®B Г?? В

2) Г?? А; Г?? B 2) ? Г?? А & В

Г?? А & В Г?? А

3) Г?? А 3) ? Г, A?? B; Г, С?? B; Г?? A U У

Г?? A U B Г?? В

4) Г, А?? 4) ? Г?? А; Г?? А

Г?? А Г??

5) Г, A, B?? C

Г, B, A?? C

6) A, A?? B 6) ? A?? B, B

A?? B A?? B

7) Г?? B 7) ? Г?? A

Г, A?? B Г?? A, B

Доведемо ?? А ® А:

1) З першої аксіоми, при Г = ? і В = А:

A ?? A

?? А ® A

Теорема доведена.

Доведемо ?? A U A

A?? A

?? A, A


?? A U A, A

?? A U A




 перетворення висловлювань |  Перетворення СДНФ в СКНФ і навпаки. |  Мінімізація висловлювань методом Квайна |  Мінімізація за допомогою карт Вейча |  функціональна повнота |  логіка предикатів |  Основні равносильности для предикатів |  отримання диз'юнктів |  Аксіоматична теорія обчислення висловлювань |  Несуперечливість і повнота аксіоматичної теорії числення висловів |

© um.co.ua - учбові матеріали та реферати