Cтраница 4
Здесь у, х и - х обозначают элементы системы объектного уровня, в данном случае - различные утверждения программы на объектном языке ( ОЯ) хорновских дизъюнктов. С другой стороны, символы выводится, Пвыводится и если являются элементами метаязыка ( МЯ), на котором мы описываем свойства системы объектного уровня. [46]
Основное достижение исследования ван Эмдена и Ковальского состоит в получении элегантных доказательств эквивалентности операционной семантики, теоретико-модельной семантики и семантики неподвижной точки для логических программ на языке хорновских дизъюнктов. Эти семантики эквивалентны в том смысле, что они определяют одни и те же денотаты для предикатных символов. Эквивалентность первых двух семантик получается благодаря теореме Геделя о полноте логики предикатов первого порядка, связывающей доказуемость с общезначимостью. Эквивалентность второй и третьей семантик устанавливается посредством доказательства того, что Ifp ( Т) есть наименьшая эрбрановская модель Р и что Р p ( t) тогда и только тогда, когда предикат p ( t) является истинным в этой модели. [47]
С другой стороны, если мы попытаемся применить резолютивный метод к соответствующим логическим предложениям, мы не сможем столь же легко добиться результата, потому что Р содержит не только хорновские дизъюнкты. [48]
В последующей статье Апт и ван Эмден ( 1982) представили семантику неподвижной точки на формальной основе теории полных решеток и с помощью этого доказали затем корректность и полноту стандартной стратегии исполнения для программ в языке хорновских дизъюнктов. Они определили также наибольшую неподвижную точку преобразования Т и использовали ее для характеризации неразрешимых программ, которые за конечное время приходят к неудаче из-за отсутствия успешных вычислений в пространстве поиска. [49]
Приблизительно в то же самое время, когда разрабатывался IC-Пролог, Перейра и Монтейро ( 1981) предложили другой интересный подход к построению логических интерпретаторов для сопрограммного и параллельного исполнения программ путем определения этих видов поведения в самой логике хорновских дизъюнктов. Они, таким образом, пришли к описаниям управления на метауровне, которые при исполнении функционируют как промежуточные интерпретаторы, сами способные извлекать эти виды поведения из стандартных логических программ объектного уровня. [50]