MPI-INF/SWS Research Reports 1991-2021

2. Number - All Departments


Towards automating duality

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

May 1993, 50 pages.

Status: available - back from printing

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.

  • 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'
  • Attachement: ATTM18XC (186 KBytes); MPI-I-93-220.pdf (240 KBytes)

URL to this document:

Hide details for BibTeXBibTeX
  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},