Towards automating duality

Dualities between different theories occur frequently in mathematics and logic—between syntax and semantics of a logic, between structures and power structures, between relations and relational algebras, to name just a few. In this paper, we show for the case of structures and power structures how corresponding properties of the two related structures can be computed fully automatically by means of quantifier elimination algorithms and predicate logic theorem provers. We illustrate the method with some examples that were computed with the theorem prover.