КАРИН

CARINE (Computer Aided Reasoning Engine) — это первого порядка, основанная на классической логике автоматизированная система доказательства теорем . Первоначально он был создан для изучения эффектов улучшения стратегий отложенного построения предложений (DCC) и последовательностей атрибутов (ATS) в алгоритме поиска в глубину. ^[1] Основным алгоритмом поиска CARINE является полулинейное разрешение (SLR), основанное на итеративном поиске в глубину (также известном как итеративное углубление в глубину (DFID)) ^[2] и используется в средствах доказательства теорем, таких как THEO. ^[3] SLR использует DCC для достижения высокой скорости вывода и ATS для уменьшения пространства поиска.

Отложенное построение статьи (DCC)

Отложенное построение предложений — это стратегия задержки, которая повышает производительность специалиста по доказательству теорем за счет сокращения работы по построению предложений до минимума. Вместо построения каждого вывода (предложения) применяемого правила вывода информация для построения такого предложения временно сохраняется до тех пор, пока средство доказательства теорем не решит либо отказаться от предложения, либо построить его. Если доказывающая теорема решит сохранить предложение, оно будет построено и сохранено в памяти, в противном случае информация, необходимая для построения предложения, будет удалена. Хранение информации, из которой может быть построено выведенное предложение, практически не требует дополнительных операций ЦП. Однако построение предложения может занять много времени. Некоторые средства доказательства теорем тратят 30–40% общего времени выполнения на создание и удаление предложений. Благодаря DCC это потерянное время можно сэкономить.

DCC полезен, когда слишком много промежуточных предложений (особенно предложений первого порядка) создаются и отбрасываются за короткий период времени, поскольку избегаются операции, выполняемые для создания таких недолговечных предложений. DCC может быть не очень эффективен для теорем, содержащих только предложения.

Как работает ДКК?

После каждого применения правила вывода некоторые переменные, возможно, придется заменить терминами (например, $x \to f (a)$ ), и таким образом формируется набор подстановок. Вместо того, чтобы создавать результирующее предложение и отбрасывать набор подстановок, средство доказательства теорем просто сохраняет набор подстановок вместе с некоторой другой информацией, например, какие предложения были задействованы в правиле вывода и какое правило вывода применялось, и продолжает вывод, не создавая результирующий результат. пункт правила вывода. Эта процедура продолжается по ходу вывода до тех пор, пока средство доказательства теорем не достигнет точки, в которой он решает, основываясь на определенных критериях и эвристиках, построить ли последнее предложение в выводе (и, возможно, некоторые другие предложения на пути) или отбросить весь вывод, т. е. удаляет из памяти поддерживаемые наборы замен и любую информацию, хранящуюся в них.

Атрибутные последовательности (ATS)

(Неформальное определение) Предложение в доказательстве теорем — это утверждение, которое может привести к истинному или ложному ответу в зависимости от оценки его литералов. Предложение представлено как дизъюнкция (т. е. ИЛИ), конъюнкция (т. е. И), множество или мультимножество (похожее на набор, но может содержать идентичные элементы) литералов.

Пример предложения как дизъюнкции литералов: $\lnot \operatorname {wealthy} (Y)\lor \lnot \operatorname {smart} (Y)\lor \lnot \operatorname {beautiful} (Y)\lor \operatorname {loves} (X,Y)$ где символы $\lor$ и $\lnot$ являются соответственно логическими или и логическими нет .

В приведенном выше примере говорится, что если Y богат, умен и красив, X любит Y. то здесь не сказано, кто такие X и Y. Однако Обратите внимание, что приведенное выше представление происходит из логического утверждения:

Для всех Y , X, принадлежащих сфере человеческих существ: $\operatorname {wealthy} (Y)\land \operatorname {smart} (Y)\land \operatorname {beautiful} (Y)\implies \operatorname {loves} (X,Y)$

Используя некоторые правила преобразования формальной логики, мы производим дизъюнкцию литералов приведенного выше примера.

X и Y — переменные. $\lnot$ богатый , $\lnot$ умный , $\lnot$ Красиво , любовь буквальна. Предположим, мы заменим переменную X на константу John и переменную Y на константу Jane, тогда приведенное выше предложение примет вид:

$\lnot \operatorname {wealthy} ({\text{Jane}})\lor \lnot \operatorname {smart} ({\text{Jane}})\lor \lnot \operatorname {beautiful} ({\text{Jane}})\lor \operatorname {loves} ({\text{John}},{\text{Jane}})$

Атрибут предложения — это характеристика предложения. Некоторые примеры атрибутов предложения:

количество литералов в предложении (т. е. длина предложения)
количество символов термина в предложении
количество констант в предложении
количество переменных в предложении
количество функций в предложении
количество отрицательных литералов в предложении
количество положительных литералов в предложении
количество различных переменных в предложении
максимальная глубина любого термина во всех литералах в предложении

Пример

пункт $C=\lnot P(x)\lor Q(a,b,f(x))$ имеет:

длина 2, потому что она содержит два литерала
- один отрицательный литерал, который $\lnot P(x)$
- один положительный литерал, который равен Q ( a , b , f ( x ))
две константы a и b
две переменные ( x встречается дважды)
одна отдельная переменная, которая равна x
одна функция, которая является f
максимальная глубина термина 2
пять терминов-символов: x , a , b , f , x

Последовательность атрибутов — это последовательность из k n кортежей атрибутов предложения, которые представляют собой проекцию набора производных значений длины k. k и n — строго положительные целые числа. Набор производных формирует домен, а последовательности атрибутов образуют кодомен отображения между производными и последовательностями атрибутов.

Пример

<(2,2),(2,1),(1,1)> — это последовательность атрибутов, где k = 3 и n = 2.

Это соответствует некоторому выводу, скажем, <(B1,B2),(R1,B3),(R2,B4)>, где B1, B2, R1, B3, R2 и B4 — предложения. Здесь предполагается, что атрибутом является длина предложения.

Первая пара (2,2) соответствует паре (B1,B2) из вывода. Это указывает на то, что длина B1 равна 2, а длина B2 также равна 2.

Вторая пара (2,1) соответствует паре (R1,B3) и указывает, что длина R1 равна 2, а длина B3 равна 1.

Последняя пара (1,1) соответствует паре (R2,B4) и указывает, что длина R2 равна 1, а длина B4 равна 1.

Примечание. Набор из n атрибутов предложения похож (но не совпадает) с вектором признаков, названным Стефаном Шульцем, доктором философии (см. E-эквациональное доказательство теоремы ).

Ссылки

^ Харун, Пол (2005). Улучшение средства доказательства теорем за счет отложенного построения предложений и последовательностей атрибутов (кандидатская диссертация). Университет Макгилла.
^ Корф, Ричард Э (1985). «Итеративное углубление в глубину: поиск оптимального допустимого дерева». Искусственный интеллект . 27 : 97–109. дои : 10.1016/0004-3702(85)90084-0 .
^ Новорожденный, Монти (2001). Автоматизированное доказательство теорем: теория и практика . Нью-Йорк: Springer-Verlag. ISBN 978-0-387-95075-4 .

Внешние ссылки

[1] Харун, Пол (2005). Улучшение средства доказательства теорем за счет отложенного построения предложений и последовательностей атрибутов (кандидатская диссертация). Университет Макгилла.

[Korf_1985-2] Корф, Ричард Э (1985). «Итеративное углубление в глубину: поиск оптимального допустимого дерева». Искусственный интеллект . 27 : 97–109. дои : 10.1016/0004-3702(85)90084-0 .

[Newborn_2001-3] Новорожденный, Монти (2001). Автоматизированное доказательство теорем: теория и практика . Нью-Йорк: Springer-Verlag. ISBN 978-0-387-95075-4 .

[1]

[2]

[3]