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

Question

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

Приветствия

Answer 1

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