Cтраница 1
Процедура опровержения, которую графически удобно представлять в виде дерева опровержения, можно применять только к формулам, имеющим стандартную форму. [1]
При доказательстве теорем обычно используют процедуры опровержения. [2]
Второй вариант теоремы Эрбрана предполагает процедуру опровержения. S и успешно устанавливать их невыполнимость, то эта процедура, как гарантируется теоремой Эрбрана, укажет нам такое конечное Л, что S невыполнимо. [3]
Поскольку метод аналитических таблиц основан на процедуре опровержения, то для доказательства общезначимости формулы X надо построить дерево ( таблицу) для ЛХ ( - Х), которое будет замкнутым. [4]
Это только вопрос удобства - при использовании процедур опровержения не происходит потери общности. Кроме того, эти процедуры опровержения применяются к стандартной форме формулы. Эта стандартная форма была введена Де висом и Патнемом [1], [ и мы будем использовать ее на протяжении всей книги. [5]
Это только вопрос удобства - при использовании процедур опровержения не происходит потери общности. Кроме того, эти процедуры опровержения применяются к стандартной форме формулы. Эта стандартная форма была введена Де висом и Патнемом [1], [ и мы будем использовать ее на протяжении всей книги. [6]
Это заключение прямо отвечает на запрос, поставленный исходным отрицанием D1, и потому оно является утверждением о решении задачи. Поскольку исходное отрицание было опровергнуто, успешный вывод называется опровержением. Методы построения опровержений называются процедурами опровержения. [7]
Дейталога требует построения дерева доказательств. Построение этого дерева можно выполнить двумя способами: 1) снизу вверх ( восходящий метод), начиная от существующих фактов и производя новые факты ( приходя, таким образом, к заключениям) и 2) сверху вниз ( нисходящий метод), пытаясь проверить истинность предпосылок, которые необходимы для проверки истинности заключения. Это различие введено в главе 7: алгоритм INFER, который вычисляет результат выполнения программы Дейталогас помощью прямого вывода, является примером восходящего метода, а процедуры резолютивного опровержения являются примерами нисходящего выполнения. Ниже мы обсудим особенности этих двух подходов с точки зрения оптимизации. [8]
Напомним, что цель есть литерал, состоящий из одного или более отрицательных литералов. Функция выбора есть отображение, соотносящее каждой цели один из ее литералов. Интуитивно выбираемый литерал - тот, который должен рассматриваться следующим в процессе реализации процедуры опровержения. [9]
Последнее обстоятельство лежит в основе тезиса Ковальского, согласно которому человеческие экспертные знания обычно не поддаются полной формализации ( являющейся, в некотором отношении, их заменой), и поэтому нет оснований надеяться, что эти знания будут иметь точную спецификацию, которой они должны соответствовать. Следует, таким образом, ожидать, что процесс введения экспертных знаний в программу для компьютера - в противоположность точной разработке хорошо специфицированных обычных программ - будет протекать посредством проб и ошибок. По мере того как база знаний развивается и к компетентности системы предъявляются новые требования, в нее должны вноситься соответствующие коррективы - точно так же и спецификацию программ возможно потребовалось бы совершенствовать для того, чтобы внести поправки и уточнения и привести ее в соответствие с новыми потребностями. По своей природе логическое программирование более, чем какой-либо другой из существующих вычислительных формализмов, приспособлено для решения задач обнаружения противоречивости ( например, с помощью процедур опровержения) и неполноты ( например, посредством правил вывода по умолчанию) с целью мотивации необходимости усовершенствования экспертной системы, в то время как метаязык логического программирования обеспечивает автоматическое описание критериев и механизмов для этого усовершенствования. [10]