Учитывая набор формул на языке TPTP, существует ли стандартный способ получения набора аксиом, который использовался для доказательства гипотезы?Это было бы примерно эквивалентно команде unsat-core
, найденной в языке SMT-LIB.
Если нет, существуют ли некоторые средства проверки TPTP или инструменты-обертки, которые предоставляют такую функциональность?