Cтраница 3
В качестве процедуры вывода используется линейная входная резолюция, которая является полной для хорновских дизъюнктов и обладает большой эффективностью. [31]
ПРОЛОГ, следуя резолютивному выводу, пытается унифицировать эту цель с заголовком некоторого хорновского дизъюнкта, содержащегося в программе. [32]
В логическом языке Пролог, в основе которого лежит принцип резолюции на базе хорновских дизъюнктов, вывод состоит в доказательстве непротиворечивости цели базе данных, состоящей из правил и фактов. [33]
Арифметико-логическая машина, базирующаяся на принципе резолюций, может выполнить алгоритм, описанный набором хорновских дизъюнктов. Язык программирования Пролог пронизан этим принципом. Пролог вводится в разд. [34]
Метод резолюций, получив на вход логическую программу с присоединенным к ней запросом в виде множества хорновских дизъюнктов, пытается построить вывод пустого дизъюнкта, обозначаемого символом D. Если это ему удается, тогда цель допускается, в противном случае отвергается. Реализуется метод резолюций с помощью двух правил: правила резолюции и правила склейки, которые во время работы вызывают процедуру унификации - сопоставления. [35]
Предложения, являющиеся отрицаниями, фактами или импликациями, образуют подкласс класса всех дизъюнктов и называются хорновскими дизъюнктами. Язык логического программирования называют иногда логикой хорновских дизъюнктов. Хорновские дизъюнкты пригодны фактически для любых целей, связанных с решением задач. Достаточность этого подкласса с точки зрения теории вычислимости обсуждается в гл. [36]
Все эти различные исследования ведут к убедительному ( впрочем, неудивительному) подтверждению того, что логика хорновских дизъюнктов является универсальным вычислительным формализмом: по вычислительной силе она эквивалентна всем другим универсальным ( и взаимно эквивалентным) формализмам, традиционно изучаемым в теории вычислимости. [37]
Применение связки - для реализации отрицания посредством неудачи не ведет к противоречиям в стандартных программах ( на хорновских дизъюнктах) и значительно расширяет ресурсы программиста. Хотя это и не дает той вычислительной силы, которой обладает логическая система со строгим отрицанием, программисты могут тем не менее без ущерба для себя читать - P ( x), как не Р ( х) при условии, что они помнят об операционном эффекте данного символа. Одна из причин уменьшения силы связки -, между прочим, состоит в том, что хотя она позволяет представлять отрицательные запросы, но не предназначается для выражения отрицательных фактов. Более общая логическая система могла бы, напротив, вычислить ответ х: 2, показывающий, что факт - ] Р ( 2) логически следует из процедур программы. [38]
Первая версия правила move является более эффективным представлением с точки зрения времени вывода, поскольку при унификации не рассматриваются хорновские дизъюнкты, если их первые два параметра не являются одинаковыми. [39]
Так как для любой программы Р: - i PU not L Р - CIRC - - программа из хорновских дизъюнктов, то стационарная ( или устойчивая) семантика такая, что АХ не содержит ни одного дизъюнкта с позитивными высказываниями, необходимо является обосновывающей. Таким образом, семантика с псевдо - или сильным отрицанием будет необходимо обосновывающей. [40]
Если какую-либо отрицательную литеру невозможно фииировать или устранить с помощью правила резолюции, то нужно вернуться и испытать следующий по порядку подходящий хорновский дизъюнкт с новыми подстановками. [41]
Мы не вводим для описания понятий более сложные логические выражения, а ограничиваемся лишь такими, которые могут быть представлены в виде хорновских дизъюнктов. Как показал Ковальски [74], применение хорновских дизъюнктов по своим изобразительным возможностям эквивалентно логике предикатов первого порядка, но позволяет реализовать эффективные алгоритмы обработки. [42]
Как мы уже отмечали, в логическом программировании приходится иметь дело с особым классом формул логики предикатов, а именно, с хорновскими дизъюнктами. [43]
Проблемы такого рода возникают всякий раз, когда мы имеем дело с предложениями, подобными Р, которые не могут быть представлены хорновскими дизъюнктами, и для которых нет возможности определить, является одна или несколько составных частей этого предложения тождественно истинной или тождественно ложной. Так, например, в нашем случае невозможно установить истинностные значения А или В. Как было показано в Определении 1.9.7, составные хорновские дизъюнкты должны содержать хотя бы одну отрицательную литеру. Это условие не соблюдается для дизъюнкта А V В, где А и В - предложения, не содержащие отрицаний. [44]
Барстолл и Дарлингтон ( 1977) предложили элегантный автоматический метод разработки программ, написанный на языке рекурсивных равенств, который во многом подобен языку логики хорновских дизъюнктов. [45]