Введение
Правило вывода в логике, теории доказательств и автоматическом доказательстве теорем В математической логике и автоматическом доказательстве теорем, разрешение - это правило вывода, ведущее к опровержению техники доказательства полных теорем для предложений в теоретической логике и логике первого порядка. Для предложений логики, систематическое применение правила разрешения действует как процедура решения для неудовлетворительности формулы, решая (дополнение) булевой задачи удовлетворительности. Для логики первого порядка разрешение может использоваться в качестве основы для полуалгоритма для проблемы неудовлетворительности логики первого порядка, обеспечивая более практичный метод, чем тот, который следует из теоремы полноты Гёделя. Правило разрешения можно проследить до Дэвиса и Путнэма (1960); однако, их алгоритм требовал попробовать все базовые экземпляры данной формулы. Этот источник комбинаторного взрыва был устранен в 1965 году алгоритмом синтаксического объединения Джона Алана Робинсона, который позволял инстанцировать формулу во время доказательства "по требованию" столько, сколько необходимо, чтобы сохранить полноту опровержения. Пункт, созданный правилом разрешения, иногда называют разрешающим.
In mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation complete theorem proving technique for sentences in propositional logic and first order logic. For propositional logic, systematically applying the resolution rule acts as a decision procedure for formula unsatisfiability, solving the (complement of the) Boolean satisfiability problem. For first order logic, resolution can be used as the basis for a semi algorithm for the unsatisfiability problem of first order logic, providing a more practical method than one following from Gödel's completeness theorem. The resolution rule can be traced back to Davis and Putnam (1960); however, their algorithm required trying all ground instances of the given formula. This source of combinatorial explosion was eliminated in 1965 by John Alan Robinson's syntactical unification algorithm, which allowed one to instantiate the formula during the proof "on demand" just as far as needed to keep refutation completeness. The clause produced by a resolution rule is sometimes called a resolvent.
Метод разрешения
В сочетании с полным алгоритмом поиска правило разрешения дает правильный и полный алгоритм для решения удовлетворительности формулы предложения и, соответственно, действительности предложения в соответствии с набором аксиомов. Эта техника разрешения использует доказательство противоречия и основывается на том факте, что любое предложение в предложении логики может быть преобразовано в эквивалентное предложение в конъюнктивной нормальной форме. Шаги следующие. Все предложения в базе знаний и отрицание предложения, которое должно быть доказано (предположение), связаны конъюнктивно. Полученное предложение преобразуется в конъюнктивную нормальную форму, причем соединения рассматриваются как элементы в наборе, S, пунктов. где является наиболее общим объединителем и , и и не имеют общих переменных.
Парамодуляция
Парамодуляция - это связанная техника рассуждения о множествах предложения, где предикатом является символ равенства. Он генерирует все "равноценные" версии предложения, за исключением рефлексивных тождеств. Операция парамодуляции принимает положительное значение из предложения, которое должно содержать буквальное равенство. Затем он ищет в предложение с подтермином, который объединяет с одной стороной равенства. Затем подтермин заменяется другой стороной равенства. Общая цель парамодуляции - уменьшить систему до атомов, уменьшая размер терминов при замещении.