z3 - Z3 TPTP証明で使用される前提/公理

Question

TPTP ファイル (例: http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Problems&Domain=SYN&File=SYN054+1.p ) で Z3 を使用する場合、どの公理を見つける方法がありますか?予想を証明するために使用されましたか？あるいは、Z3 は TPTP プルーフを作成できますか?

乾杯

Answer 1

Z3 には、限定的な TPTP サポートが含まれています。公理名を追跡したり、TPTP 形式で証明を生成したりしません。Z3 は SMT-LIB2 形式の豊富なサポートを提供し、SMT-LIB2 パーサーで消化できる形式でプルーフを生成します。