прогр реал преобр формата TPTP или DFG в пренексную форму

[alex_dorin]

Здравствуйте !

Подскажите существующую програмную реализацию для преобразования формулы логики первого
порядка из формата TPTP или DFG в пренексную форму (без сколемизации).

С уважением Александр Дорин

[arseniiv]

TPTP — этот? Так там формулы не обязательно логики первого порядка будут.

[alex_dorin]

Да, интересуют только формулы первопорядковой логики c равенством.

[arseniiv]

Ну, грамматика такого подмножества языка будет попроще, можно и своим кодом разбирать. Может, напишете парскер быстрее, чем дождётесь другого ответа.