TOWARDS AUTOMATING DUALITY

Dualities between different theories occur frequently in mathematics a nd logic-between syntax and semantics of a logic, between structures a nd power structures, between relations and relational algebras, to nam e just a few. In this paper, we show for the case of structures and po wer structures how corresponding properties of the two related structu res can be computed fully automatically by means of quantifier elimina tion algorithms and predicate logic theorem provers. We illustrate the method with some examples that were computed with the Otter theorem p rover.