  To support reasoning about properties of programs operating with boolean
values one needs theorem provers to be able to natively deal with the boolean
sort. This way, program properties can be translated to first-order logic and
theorem provers can be used to prove program properties efficiently. However,
in the TPTP language, the input language of automated first-order theorem
provers, the use of the boolean sort is limited compared to other sorts, thus
hindering the use of first-order theorem provers in program analysis and
verification. In this paper, we present an extension FOOL of many-sorted
first-order logic, in which the boolean sort is treated as a first-class sort.
Boolean terms are indistinguishable from formulas and can appear as arguments
to functions. In addition, FOOL contains if-then-else and let-in constructs. We
define the syntax and semantics of FOOL and its model-preserving translation to
first-order logic. We also introduce a new technique of dealing with boolean
sorts in superposition-based theorem provers. Finally, we discuss how the TPTP
language can be changed to support FOOL.
