我正在使用SMT-LIB中的Int来定义时间步骤，这迫使我断言事情以确保在否定中没有发生任何事情：
(declare-sort Pkg) ; A package
(define-sort Time () Int) ; The installation step
; ...
(assert (forall ((t Time) (p Pkg)) (=> (< t 0) (not (installed p t)))))
我在Z3中看到，我们可以用通常的方式定义归纳Nats。使用Nat的归纳定义是否合适？还是有更好的方法来做我上面尝试做的事情？
你应该坚持Int，并适当地加入>= 0约束。 Z3对Int了解很多，有各种各样的证明规则和技巧来处理它。虽然你确实可以定义一个归纳的Nat类型，但你将失去处理整数的所有内部机制，并且由于递归定义，Z3的决策程序效率会降低;特别是与其他理论相结合。
话虽如此，除非您尝试，否则无法知道：可能存在一些问题域，其中归纳定义可能更适合。但仅仅通过纯粹看待你处理的那种问题，好的老Int似乎是你的正确选择。
另请参阅此相关问题：Representing temporal constraints in SMT-LIB在您的上下文中绝对相关。