КАРИН

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

Строительство с отложенным условием (DCC)

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

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

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

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

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

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

Примером предложения как дизъюнкции литералов является: где символы и являются, соответственно, логическим ИЛИ и логическим НЕ . $\lnot \operatorname {богатый} (Y)\lor \lnot \operatorname {умный} (Y)\lor \lnot \operatorname {красивый} (Y)\lor \operatorname {любит} (X,Y)$ $\лор$ $\lnot$

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

Для всех Y , X, принадлежащих к области человеческих существ: $\operatorname {богатый} (Y)\land \operatorname {умный} (Y)\land \operatorname {красивый} (Y)\implies \operatorname {любит} (X,Y)$

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

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

$\lnot \operatorname {богатый} ({\text{Джейн}})\lor \lnot \operatorname {умный} ({\text{Джейн}})\lor \lnot \operatorname {красивый} ({\text{Джейн}})\lor \operatorname {любит} ({\text{Джон}},{\text{Джейн}})$

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

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

Пример

в статье есть: $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. doi :10.1016/0004-3702(85)90084-0.
^ Newborn, Monty (2001). Автоматизированное доказательство теорем: теория и практика . Нью-Йорк: Springer-Verlag. ISBN 978-0-387-95075-4.

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

Веб-сайт CARINE
Публикация ACM
Домашняя страница E