z3 - Z3 TPTP 证明中使用的前提/公理

Question

在 TPTP 文件上使用 Z3 时（例如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 解析器可以消化的格式生成证明。