Есть ли прувер только для логики высказываний

Question

Я попытался реализовать логику LTL c синтаксически, используя команду аксиоматизации, с целью автоматического поиска доказательств для теорем (мотивация доказательства свойств программы).

Однако все автоматы c, такие как (cvc4, z3, e, et c), используют квантификаторы некоторого рода. Например, используя FOL, можно доказать F (p) -> G (p), что, очевидно, неверно.

Мой вопрос заключается в том, существует ли доказатель, такой же, как упомянутые, но который сделан для пропозиционального logi c, т.е. имеет доступ только к MP и пропозициональным логикам c аксиом.

Я довольно новичок в Изабель, так что, возможно, есть более простой способ сделать это, я не вижу.

РЕДАКТИРОВАТЬ: Я ищу доказательство дедукции в стиле Гильберта, а не SAT, как это было бы победить проблему его реализации аксиоматически

Answer 1

Что вам нужно, так это SAT-решатель, такой как minisat .

Однако все автоматы c, такие как (cvc4, z3, e, et c), используют квантификаторы некоторого рода. Например, используя FOL, можно доказать F (p) -> G (p), что, очевидно, неверно.

Это не правильно. Любой испытатель теорем первого порядка, как iProver, E, Vampire, будет не доказывать forall X. f(X) => g(x).

Answer 2

Я думаю, что метод sat использует только логики высказываний c.

Однако я бы порекомендовал не использовать аксиоматизацию, а просто определить синтаксис LTL с использованием типов данных и семантику с использованием функций. Возможно, вы можете повторно использовать формализацию из https://www.isa-afp.org/entries/LTL.html

Без аксиоматизации вы можете использовать любой метод.