| Abstract: | Automated analysis and verification of programs requires proving properties in the combination of first-order theories of various data structures, such as integers, arrays, or lists. Automated first-order theorem provers face new requirements from reasoning-based analysis and verification, and their efficiency largely depends on how programs are translated into a collection of logical formulas capturing the program semantics.
Recent extentions to the TPTP language, the input language of automated provers, support new programming languages features aimed to keep translation-sensitive semantics on the level
of the theorem prover. For example, TPTP has recently been extended with if-then-else and let-in constructs over terms and formulas. In this paper we propose to extend TPTP with
the built-in first class boolean type that can facilitate translation
of programs with conditional statement and simplify the treatment of if-then-else and let-in constructs of TPTP.
The treatment of a built-in first class boolean type can
be efficiently implemented in the Vampire theorem prover without major changes in
its architecture. |
