Логические пруверы логики 1-го порядка и NBG

[alex_dorin]

Здравствуйте !
Возможно ли использовать логические пруверы для первопорядковой логики, именно Vampire, E, Spass
для доказательства теорем в теории множеств NBG ?
Наверное, этого делать нельзя из-за использования в NBG индивидных переменных 2-х сортов.
Верен ли мой такой вывод ? Обязательно ли преобразовывать все аксиомы NBG и гипотезы с использованием индивидных переменных одного сорта ?
C уважением,
Александр А. Дорин

[arseniiv]

Странный вопрос.
1. На него должна ответить документация по тем системам.
2. Если всё плохо, то, разумеется, преобразуйте к виду с переменными одного сорта, а лучше просто найдите такое представление — оно уже очень давно где-нибудь должно быть выписано.

Хотя, конечно, на форуме могут оказаться люди, которые лучше вас знают Vampire, E и Spass.

-- Вт ноя 17, 2015 20:44:11 --

(А что стало с ZFC?)