Я хочу использовать ATP для определения того, является ли данная формула непротиворечивой или нет, без предположений, например: ! [X] : P(X) & ~P(X) не является непротиворечивым (в синтаксисе tptp).
Подключение таких формул к вампиру:
fof(test, conjecture,! [X] : P(X) & ~P(X)).
Урожайность "сатинируема".То же самое для:
![X]: ![Y]: X=Y
Кажется, что я упускаю что-то простое из-за того, как оно работает, или значения "выполнимо".Я не смог найти источник для формата tptp, так что, возможно, моя проблема там.
Любая помощь будет приветствоваться.