hide
Free keywords:
-
Abstract:
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 a large number of examples and we give
enough technical hints to enable the reader who has access to the {\sc
Otter} theorem prover
to experiment herself.
