# Author:Simon Robillard

### Keyphrases

acyclicity, automated reasoning^{2}, automated theorem proving, consequence finding, first-order logic, first-order theorem proving, inference rule, invariant generation^{3}, loop, polymorphic arrays, program analysis^{2}, program verification^{2}, superposition, symbol elimination, term algebra, termination.