Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

MPI-I-93-220

Towards automating duality

Brink, Chris and Gabbay, Dov M. and Ohlbach, Hans J├╝rgen

MPI-I-93-220. May 1993, 50 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
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.
Acknowledgement:
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-93-220.pdfMPI-I-93-220.pdf MPI-I-93-220.dvi Article: Database 'MPII AG2 Publications', View '1. Author/Editor \ 1. by Individual', Document 'Description Logics for Natural Language Processing'186 KBytes; 240 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
URL to this document: http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1993-220
Hide details for BibTeXBibTeX
@TECHREPORT{BrinkGabbayOhlbach93,
  AUTHOR = {Brink, Chris and Gabbay, Dov M. and Ohlbach, Hans J{\"u}rgen},
  TITLE = {Towards automating duality},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-93-220},
  MONTH = {May},
  YEAR = {1993},
  ISSN = {0946-011X},
}