About Tseitin's transformation in logical equations.pdf В 1968 г. в журнале «Записки научных семинаров ЛОМИ» вышла статья ГригорияСамуиловича Цейтина «О сложности вывода в исчислении высказываний» [1]. Сегодняможно с уверенностью сказать, что эта выдающаяся и совершенно новаторская на тотмомент работа намного опередила время и предвосхитила целый спектр направленийв логике и теории алгоритмов.Основным инструментом [1] являются очень простые по своей природе преобразованиялогических выражений. Далее приведены две цитаты из [1], в которых описаныданные преобразования.«Исчисления, которыми мы будем пользоваться, направлены на установлениепротиворечивости систем дизъюнкций. Понятие противоречивой системы дизъюнкцийслужит здесь аналогом понятия тождественно истинной формулы в обычномисчислении высказываний. От вопроса о тождественной истинности заданной формулыисчисления высказываний можно перейти к вопросу о противоречивости некоторойсистемы дизъюнкций, приведя отрицание данной формулы к конъюнктивнойнормальной форме. Однако при таком преобразовании может резко возрасти длинаформулы, поэтому мы будем рассматривать другой способ перехода от формулыисчисления высказываний к системе дизъюнкций. Каждой подформуле данной формулыпоставим в соответствие свою переменную; двум подформулам будут соответствоватьсопряженные переменные1 в том и только том случае, если одна изэтих формул является отрицанием второй. Если некоторая подформула A представляетсобой конъюнкцию подформул B и Г и этим подформулам приписаны соответственнопеременные а, в и Y, то припишем подформуле A следующую системудизъюнкций2: аД,

Скачать электронную версию публикации