Хорошая справка о приближенных методах решения логических задач

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

Таким образом, можно ожидать, что приближенные алгоритмы для логических задач также могут быть подходящими. Однако единственная тенденция к поиску в этом направлении, которую мне удалось обнаружить, - это проблема max-SAT, и ее развитие было активно в девяностые годы.

Существуют ли другие активные направления исследований, семинары, ключевые слова, хорошие ссылки для использования и разработки приближенных методов для модальной логики, логического программирования и так далее?

Если ожидается, что автоматическое рассуждение получит видное место в будущих приложениях информатики, тогда нужно будет выйти за пределы неразрешимых логических ограничений, и приближенные методы или эвристики могут быть естественным путем, не так ли?

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

Полезно различать понятия аппроксимации.

• $\varepsilon$
• $\delta$

$(\varepsilon,\delta)$

Вот пример другого понятия приближения. Предположим, вы выполняете вычисление, например, умножаете два больших числа и хотите проверить, правильно ли это умножение. Существует множество эвристических методов, которые используются на практике для проверки правильности без повторения расчета. Вы можете проверить, что знаки были умножены, чтобы получить правильный знак. Вы можете проверить, имеют ли числа правильную четность (свойства четного / нечетного числа). Вы можете использовать более сложную проверку, такую ​​как « Изгнание девяток»., Все эти методы имеют общее свойство, которое они могут сказать вам, если вы допустили ошибку, но они не могут гарантировать, что вы получили правильный ответ. Это свойство можно рассматривать как логическое приближение, поскольку вы можете доказать, что первоначальный расчет неверен, но вы не сможете доказать, что он правильный.

Все проверки, которые я упомянул выше, являются примерами техники, называемой абстрактной интерпретацией. Абстрактная интерпретация делает строгое понятие логического приближения отличным от числового и вероятностного приближений. Проблема, которую я описал с анализом одного вычисления, распространяется на более сложный случай анализа программы. Литература по абстрактной интерпретации разработала методы и рамки для приблизительных, логических рассуждений о программах и, в последнее время, о логике. Следующие ссылки могут быть полезны.

1. Абстрактная интерпретация в двух словах Патрика Кузо, простой обзор.
2. Обзор абстракции Патрика Кузо, как часть его курса. Есть очень хороший пример абстракции для определения свойств букета цветов. Аналогия с букетом включает в себя фиксированные точки и может быть сделана полностью математически точной.
3. Курс по абстрактной интерпретации Патрика Кузо, если вы хотите всю глубину и детали.
4. Абстрактная интерпретация и применение к логическим программам , Patrick Cousot и Radhia Cousot, 1992. Применяется к логическим программам согласно вашему запросу. Первоначальный раздел также формализует процедуру изгнания девяток как абстрактную интерпретацию.

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

1. Обобщение метода Штальмарка Адитьей Тхакуром и Томасом Репсом, 2012. Дает обобщение метода Стальмарка на проблемы в программном анализе.
2. Сокращенное произведение абстрактных доменов и комбинация процедур принятия решений , Патрик Кузо, Радия Кузо и Лоран Моборгн, 2011. В этой статье рассматривается метод Нельсона-Оппена для объединения процедур принятия решений и показано, что его также можно использовать для неполных комбинаций, которые особенно интересно, если у вас есть неразрешимые проблемы.
3. Решатели удовлетворенности - это статические анализаторы , моя статья с Леопольдом Халлером и Даниэлем Крёнингом, 2012. Применяет представление приближений на основе решеток для характеристики существующих решателей. Вы также можете посмотреть мои слайды по теме .

Теперь ни одна из вышеприведенных статей не отвечает на ваш конкретный вопрос о том, как атаковать проблемы удовлетворяемости, которые неразрешимы. В этих работах рассматривается аппроксимативно-ориентированный взгляд на логические проблемы, который не является числовым или вероятностным. Эта точка зрения широко применялась к рассуждениям о программах, и я считаю, что она точно соответствует вашим запросам.

Чтобы применить его к модальной логике, я бы предложил использовать алгебраическую семантику Йонссона и Тарского или более позднюю семантику Леммона и Скотта. Это связано с тем, что абстрактная интерпретация формулируется в терминах решеток и монотонных функций, поэтому булевы алгебры с операторами представляют собой удобную семантику для работы. Если вы хотите начать с фреймов Крипке, вы можете применить теорему двойственности Йонссона и Тарского (которую некоторые могут назвать дуальностью Стоуна) и получить алгебраическое представление. После этого вы можете применить теоремы абстрактной интерпретации для логического приближения.