"Моделирование рассуждений. Опыт анализа мыслительных актов" - читать интересную книгу автора (Поспелов Дмитрий Александрович)«Логик-теоретик»Так была названа программа для ЭВМ, созданная в середине шестидесятых годов американским кибернетиком А. Ньюэллом в содружестве с психологом Г. Саймоном. Она была предназначена для доказательства теорем в исчислении высказываний, т.е. для поиска обоснования тождественной истинности некоторых утверждений. Для того чтобы перейти к описанию программы «Логик-теоретик», введем предварительно понятие о равенстве двух выражений исчисления высказываний. Будем говорить, что выражения ?1 и ?2 равны между собой, и записывать этот факт обычным образом ?1=?2, если на всех возможных наборах интерпретации истинности входящих в них элементарных высказываний истинность ?1 и ?2 одинакова. Появление знака равенства, которого не было в исчислении высказываний, не должно нас смущать. Его легко можно исключить из рассмотрения, введя формулу ((?1amp;?2) «Логик-теоретик» должен был доказывать справедливость утверждений вида ?1=?2 для различных ?1 и ?2. Однако авторы «Логика-теоретика» не пошли по прямому пути. Не стали строить таблицы для ?1 и ?2 и проверять совпадение истинности ?1 и ?2 на всех возможных интерпретациях истинности их аргументов. Ведь с ростом числа аргументов В основу процесса доказательства они положили идею ликвидации различий в формульной записи ?1 и ?2. Авторы программы составили перечень из шести различий. 1. В ?1 и ?2 различное число членов в формулах. Например, ?1=? 2. В ?1 и ?2 имеется различие в основной связке (т.е. в связке, которая выполняется последней). Например, ?1=(??) 3. Перед всем выражением для ?1(?2) стоит знак отрицания, а перед ?2(?1) его нет. Например, ?1= 4. Аналогичное различие, но оно касается не всего выражения для ? 5. Скобки в ?1 расставлены не так, как в ?2. Например, ?1=? 6. Записи для ?1 и ?2 отличаются порядком следования подвыражений. Например, ?1=(??) Для того чтобы иметь возможность ликвидировать подобные различия, используются 12 преобразований формул исчисления высказываний. Первые семь преобразований носят тождественный характер, т.е. не меняют истинного значения преобразуемых формул. Последние пять верны только при условии, что левая часть их является тождественно истинной ( В преобразованиях использованы большие латинские буквы, которые могут соответствовать любым подвыражениям формул ?1 и ?2. Стрелки С помощью этих преобразований можно устранять различия между ?1 и ?2, которые мы перечислили выше. Укажем в специальной табл. 4 классы преобразований Таблица 4 Крестики поставлены там, где можно устранить различие с помощью соответствующего преобразования. Покажем работу программы «Логик-теоретик» на несложном примере. Пусть требуется доказать равенство ?1=?2, имеющее вид Применим к ?1 первое преобразование из Поскольку в ?1 осталось еще выражение Теперь можно применить второе преобразование из Четвертое преобразование из Пример, конечно, не отражает всех особенностей работы программы «Логик-теоретик». Мы несколько упростили задачу. Как видно из таблицы различий, выбор преобразования на каждом шаге далеко не однозначен. В формулах могут существовать одновременно несколько различий, а для ликвидации различия можно использовать несколько преобразований. Всякий вывод, как бы он не был организован, носит переборный характер. И успешность того или иного выбора преобразования не может быть оценена локально, в момент выбора. Поэтому программа вынуждена перебирать варианты, заходить в тупики, проходить циклы прежде, чем она сможет найти правильный путь решения. Повышение эффективности процесса вывода – центральная проблема всех автоматизированных систем дедуктивного вывода. |
||||||||||||||||
|