Athena and model generation

Athena is seamlessly integrated with Paradox, an efficient model generator for first-order logic. Model generation is very useful for consistency checking, and in particular for falsifying conjectures: If we are not sure whether a formula follows from a given set of premises (e.g. suppose that an ATP cannot show this, and we cannot think of a proof ourselves), we can try to find a counter-model, i.e., a model in which all the premises are true but the formula in question is false. Model generators can be used to find such models automatically. For more information on how this can be done or why it is useful, take a look at this paper. In Athena an invocation of Paradox is just a function call, so the user can easily write code that calls the model finder as frequently as necessary and with dynamically varying arguments. This is more flexible and convenient than using model finders in their normal batch-oriented mode from the command line (or with scripts).