@article{BGO94, 
AUTHOR  	 =  "Chris Brink and Dov Gabbay and Hans J{\"u}rgen Ohlbach",
TITLE = "Towards Automating Duality",
journal = "Journal of Computers and Mathematics with Applications",
year    = 1994, 
volume  = 29,
number  = 2,
pages   = "73--90",
note = "A longer version appeared as a technical report MPI-I-93-220 of the Max-Planck-Institut f{\"u}r Informatik, Saarbr{\"u}cken, Germany.",
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.},
keywords = {Quantifier Elimination, Duality Theory, Correspondence Theory},
source = "ftp://pub/guide/staff/ohlbach/publications/articles/duality.dvi.gz"}}