z3 - Z3py 是否支持线性时间逻辑 LTL？

Question

Z3py 是否支持线性时间逻辑 LTL？如果是，您能否提供一个简单解释的示例。

Answer 1

Z3 不支持 LTL 或其他时间或模态逻辑。Z3接受的输入是一阶逻辑，有算术等理论。