I am trying to model some hardware in first-order logic using the automated theorem prover SPASS.
So I'd need signals that can take true/false values (the pre-defined ones) in order to be able to use them in logic sentences.
SPASS supports some kind of types (called sorts) which the user can define himself.
I'm wondering if there is some pre-defined type for true/false?
I think I can work around this even without the type.. by using a predicate of the form True(SIGNAL) and False(SIGNAL) and make True(SIGNAL) return true when SIGNAL = T and false when SIGNAL = F (T and F are constants), but I think it would have been nicer to use the pre-defined true/false.