Cтраница 1
Логик-теоретик явился реализацией идеи о том, что можно составить программы, которые решали бы задачи подобно тому, как это делает человек. [1]
Логик-теоретик - программа для вычислительной машины, которая находит доказательства теорем математической логики ( перечисленных в гл. [2]
Логик-теоретик был запрограммирован Ньюэллом, Шоу и Саймоном в начале 1956 г. Это была первая эвристическая программа, полностью реализованная на вычислительной машине, первая попытка проникнуть в сложные процессы мышления с помощью исследований в области искусственного разума. [3]
Логик-теоретик и машина для игры в шахматы Ньюэлла, Шоу и Саймона [789, 792] и геометрическая машина Гелерн-тера и Рочестера [363] являются примерами работающих эвристических программ в других областях. [4]
Логик-теоретик Ньюэлла, Шоу и Саймона [117]), которые выносят главные решения непосредственно на языке структурных характеристик рассматриваемой задачи. [5]
Как и Логик-теоретик Ньюэлла, Шоу и Саймона, геометрическая машина для достижения этой цели опирается на хорошо известный аналитический метод. Метод обратного просмотра гарантирует машине, что каждая рассматриваемая ею последовательность действительно оканчивается на требуемом утверждении. Однако само по себе это без использования дополнительных эвристик не представляет значительного улучшения по сравнению с полным перебором, ибо преимущества метода обратного просмотра покупаются дорогой ценой, так как нет никакой гарантии, что каждая вырабатываемая последовательность, оканчивающаяся нужным образом, вообще служит доказательством чего-либо. Действительно, большинство цепочек, полученных таким способом, будут ложными. Но именно в этом и состоит сила аналитического метода, так как, если бы оказалось возможным найти способ обнаружения ложных последовательностей, такие последовательности можно было бы немедленно отбрасывать, что позволило бы отсекать от богато разветвленного дерева решений сухие ветви. Набор последовательностей, вырабатываемых таким процессом, содержал бы на любой глубине поиска на несколько порядков меньше членов, и плотность возможных доказательств теоремы среди этих последовательностей была бы соответственно выше. [6]
Наши исследования машины Логик-теоретик являются звеном в общей программе исследования сложных систем переработки информации. [7]
Эти программы получили названия Логик-теоретик ( Logic Theorist-LT) и Общий решатель задач ( General Problem Solver-GPS); они содержали общие процедуры поиска стратегий ( или доказательства теорем и ведения игр) и имели впечатляющий, хотя и ограниченный успех. GPS была неспособна доказать неразрешимость задачи о кенигсбергских мостах или научиться хорошо играть в шахматы. [8]
Интересно отметить, что работа над программой Логик-теоретик привела к созданию первого машинного языка для работы со списками символов, что имело большое значение для исследований по искусственному разуму и вообще для наук, связанных с вычислительными машинами. [9]
В 1957 г. Ыьюэлл, Шоу и Саймон опубликовали описание программы Логик-теоретик, представляющей собой систему обработки информации для решения таких задач, которые до того времени было под силу решать только человеческому разуму. [10]
Одна из первых работ в области эвристического программирования была посвящена разработке программы Логик-теоретик для доказательства математических теорем. В программе логик-теоретик практически реализована возможность автоматизированного доказательства математических теорем символической логики, а именно, теорем по исчислению высказываний. Программа Логик-теоретик на основании правил вывода позволяет получать новые теоремы из исходных аксиом и других теорем. [11]
Одна из первых работ в области эвристического программирования была посвящена разработке программы Логик-теоретик для доказательства - математических теорем. В программе Логик-теоретик практически реализована возможность автоматизированного доказательства математических теорем символической логики, а именно - теорем по исчислению высказываний. Программа Логик-теоретик на основании правил вывода позволяет получать новые теоремы из исходных аксиом и других теорем. В доказательстве используют три правила вывода: подстановку, замену, отделение, а в качестве аксиом - пять истинных высказываний. Построение доказательства начинают от конечного результата по направлению к исходным посылкам. Эта направленность доказательства и вопросы иерархического наследования в доказательстве теорем имеют ряд общих черт с процедурой синтеза структуры ХТС. На каждом этапе из заданного списка аксиом или ранее доказанных теорем выбирается такая, из которой с помощью правил вывода может быть выведена теорема данного этапа. Поэтапная процедура доказательства продолжается до тех пор, пока в списке для вывода не окажутся исходные посылки. В этом случае задача считается решенной. Необходимо, однако, отметить, что в ряде случаев поиск метода доказательства теоремы может оказаться безуспешным. [12]
Одна из первых работ в области эвристического программирования была посвящена разработке программы Логик-теоретик для доказательства математических теорем. В программе логик-теоретик практически реализована возможность автоматизированного доказательства математических теорем символической логики, а именно, теорем по исчислению высказываний. Программа Логик-теоретик на основании правил вывода позволяет получать новые теоремы из исходных аксиом и других теорем. [13]
Так, Логик-теоретик может применять тот же набор эвристик при доказательстве производного выражения, как и при доказательстве исходного положения, из которых оно было выведено. [14]
Одна из первых работ в области эвристического программирования была посвящена разработке программы Логик-теоретик для доказательства - математических теорем. В программе Логик-теоретик практически реализована возможность автоматизированного доказательства математических теорем символической логики, а именно - теорем по исчислению высказываний. Программа Логик-теоретик на основании правил вывода позволяет получать новые теоремы из исходных аксиом и других теорем. В доказательстве используют три правила вывода: подстановку, замену, отделение, а в качестве аксиом - пять истинных высказываний. Построение доказательства начинают от конечного результата по направлению к исходным посылкам. Эта направленность доказательства и вопросы иерархического наследования в доказательстве теорем имеют ряд общих черт с процедурой синтеза структуры ХТС. На каждом этапе из заданного списка аксиом или ранее доказанных теорем выбирается такая, из которой с помощью правил вывода может быть выведена теорема данного этапа. Поэтапная процедура доказательства продолжается до тех пор, пока в списке для вывода не окажутся исходные посылки. В этом случае задача считается решенной. Необходимо, однако, отметить, что в ряде случаев поиск метода доказательства теоремы может оказаться безуспешным. [15]