Abstract. An extension of the superposition-based E-prover [8] is described. The extension allows terms with integer exponents [3] in the input language. Obviously, this possibilit...
Interpolation is an important technique in verification and static analysis of programs. In particular, interpolants extracted from proofs of various properties are used in invar...