 Популярные статьи | |
| Сейчас на сайте |  Гостей: 2
На сайте нет зарегистрированных пользователей
Пользователей: 9,955
новичок: Logyattella
|
|
| «Логик-теоретик» |
показывают направление преобразований. (Знак
есть по сути знак
.)
С помощью этих преобразований можно устранять различия между ? 1 и ? 2 , которые мы перечислили выше. Укажем в специальной табл. 4 классы преобразований F 1 , которые можно использовать для устранения различий. Первое различие разделено на два: различие 1 ’ требует добавления выражений в формулу, а различие 1 ’’ – вычеркивания из формулы лишних выражений.
Таблица 4
Крестики поставлены там, где можно устранить различие с помощью соответствующего преобразования.
Покажем работу программы «Логик-теоретик» на несложном примере. Пусть требуется доказать равенство ? 1 =? 2 , имеющее вид
Применим к ? 1 первое преобразование из F 7 справа налево. Выбор F 7 определяется различием ? 1 и ? 2 . Из ? 1 необходимо убрать лишнее подвыражение С , которого нет в ? 2 . После этого получим
Поскольку в ? 1 осталось еще выражение С , которого нет справа, то снова фиксируется различие 1 ’’ и ищется подходящее преобразование. Таким преобразованием является четвертое из F 7. Но для его применения надо сначала использовать преобразование F 1 для устранения различия 6. После этого, применяя четвертое преобразование из F 7, получаем
Теперь можно применить второе преобразование из F 7:
Четвертое преобразование из F 7 приводит к окончательному результату
Пример, конечно, не отражает всех особенностей работы программы «Логик-теоретик». Мы несколько упростили задачу. Как видно из таблицы различий, выбор преобразования на каждом шаге далеко не однозначен. В формулах могут существовать одновременно несколько различий, а для ликвидации различия можно использовать несколько преобразований. Всякий вывод, как бы он не был организован, носит переборный характер. И успешность того или иного выбора преобразования не может быть оценена локально, в момент выбора. Поэтому программа вынуждена перебирать варианты, заходить в тупики, проходить циклы прежде, чем она сможет найти правильный путь решения. Повышение эффективности процесса вывода – центральная проблема всех автоматизированных систем дедуктивного вывода.
|
|
| Комментарии |
| Добавить комментарий |
|
Пожалуйста залогиньтесь для добавления комментария.
|
| Рейтинги |
|
Рейтинг доступен только для пользователей.
Пожалуйста, залогиньтесь или зарегистрируйтесь для голосования.
Нет данных для оценки.
|
|
| Гость |
Вы не зарегистрированны? Нажмите здесь для регистрации.
Забыли пароль? Запросите новый здесь.
|
| Мини-чат | Вам необходимо залогиниться.
Нет присланных сообщений.
|
|
