Используемые помещения/аксиомы в Z3 TPTP-доказательствах

Question

При использовании Z3 в файлах TPTP (например, http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Problems&Domain=SYN&File=SYN054+1.p) есть ли способ узнать, какие аксиомы использовались для доказательства гипотезы? В качестве альтернативы, может ли Z3 выдавать доказательства TPTP?

Cheers

Answer 1

Z3 включает в себя ограниченную поддержку TPTP. Он не отслеживает имена аксиом или не дает доказательств в формате TPTP. Z3 предлагает богатую поддержку формата SMT-LIB2 и производит доказательства в формате, который можно переваривать анализаторами SMT-LIB2.