我正在尝试使用自动定理证明器 SPASS 在一阶逻辑中对一些硬件进行建模。
所以我需要可以采用真/假值（预定义的值）的信号，以便能够在逻辑语句中使用它们。
SPASS 支持用户可以自己定义的某种类型（称为排序）。
我想知道是否有一些预定义的真/假类型？
我想即使没有类型，我也可以解决这个问题。通过使用 True(SIGNAL) 和 False(SIGNAL) 形式的谓词，并在 SIGNAL = T 时使 True(SIGNAL) 返回 true，在 SIGNAL = F (T 和F 是常量），但我认为使用预定义的真/假会更好。