在Z3 TPTP證明中使用的房屋/公理

Question

在TPTP文件（例如http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Problems&Domain=SYN&File=SYN054+1.p）上使用Z3時，是否有辦法找出哪些公理用於證明猜測？另外，Z3可以生產TPTP證明嗎？

Cheers

Answer 1

Z3包括有限的TPTP支持。 它不會跟蹤公理名稱或以TPTP格式生成證明。 Z3爲SMT-LIB2格式提供了豐富的支持，並以可由SMT-LIB2解析器消化的格式生成樣本 。