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).