RAIRO - Theoretical Informatics and Applications

Table of Contents - April 2012 - Volume 46, Issue 02 (12th Italian Conference on Theoretical Computer Science (ICTCS))  

Research Article

A graphical representation of relational formulae with complementation ∗

Domenico Cantonea1, Andrea Formisanoa2, Marianna Nicolosi Asmundoa1 and Eugenio Giovanni Omodeoa3

a1 Dipartimento di Matematica e Informatica, Università di Catania, Viale Andrea Doria 6, 95125 Catania, Italy. cantone@dmi.unict.it; nicolosi@dmi.unict.it

a2 Dipartimento di Matematica e Informatica, Università di Perugia, Via Vanvitelli 1, 06123 Perugia, Italy; formis@dmi.unipg.it

a3 Dipartimento di Matematica e Informatica, Università di Trieste, Via Valerio 12/1, 34127 Trieste, Italy; eomodeo@units.it

Abstract

We study translations of dyadic first-order sentences into equalities between relational expressions. The proposed translation techniques (which work also in the converse direction) exploit a graphical representation of formulae in a hybrid of the two formalisms. A major enhancement relative to previous work is that we can cope with the relational complement construct and with the negation connective. Complementation is handled by adopting a Smullyan-like uniform notation to classify and decompose relational expressions; negation is treated by means of a generalized graph-representation of formulae in ℒ+, and through a series of graph-transformation rules which reflect the meaning of connectives and quantifiers.

(Received December 21 2010)

(Accepted January 17 2012)

(Online publication February 27 2012)

Key Words:

  • Algebra of binary relations;
  • quantifier elimination;
  • graph transformation

Mathematics Subject Classification:

  • 68Q40;
  • 68T15;
  • 03C10

Footnotes

∗  This research is partially supported by GNCS-10, GNCS-11, and PRIN-08 projects, and by grants 2009.010.0336 and 2010.011.0403. We would like to thank the anonymous referees for their useful suggestions.