Состояние искусства для монадического класса?

11

В монадической логике первого порядка, также известной как монадический класс задачи решения, все предикаты принимают один аргумент. Аккерманн показал, что он может быть разрешен и НЕОБХОДИМО завершен .

Однако такие проблемы, как SAT и SMT, имеют быстрые алгоритмы их решения, несмотря на теоретические ограничения.

Мне интересно, есть ли исследования, аналогичные SAT / SMT для монадической логики первого порядка? Что такое «уровень техники» в этом случае, и существуют ли алгоритмы, которые эффективны на практике, несмотря на нарушение теоретических ограничений в худшем случае?

jmite
источник

Ответы:

3

Я обнаружил признаки того, что такая процедура принятия решения была реализована в (общем) доказательстве теоремы SPASS .

В частности, см. Тезис Анн-Кристин Нолл « О процедурах принятия решений по разрешению для монадического фрагмента и охраняемого фрагмента отрицания». Это реализует то, что вы хотите, хотя я не мог найти реализацию в Интернете.

Коди
источник
2

В 1993 году в статье LICS Бахмайр, Ганзингер и Вальдман показали, что ограничения на множество эквивалентны монадическому FOL, а на множестве - это монадический класс . Если память служит, установленные ограничения эквивалентны обычным древовидным грамматикам, поэтому большинство разработанных там алгоритмов также должны переноситься на монадические FOL.

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

Нил Кришнасвами
источник
Да ... Я признаю, что мой интерес к монадическому классу заключается в решении ограничений набора, поэтому у нас возникла проблема курицы и яйца. Большая часть того, что я нашел для установленных ограничений в программном анализе, таких как Banshee, относится к ограниченным классам, которые слабее монадического класса (то есть они не имеют отрицания или проекции). Но я мог пропустить кучу.
Jmite