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

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

Ваше здоровье


z3
person user1226336    schedule 22.02.2012    source источник

Ответы (1)


arrow_upward
3
arrow_downward

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

person Nikolaj Bjorner    schedule 24.02.2012