a1 Dipartimento di Matematica e Informatica, Università di Catania, Viale Andrea Doria 6, 95125 Catania, Italy. firstname.lastname@example.org; email@example.com
a2 Dipartimento di Matematica e Informatica, Università di Perugia, Via Vanvitelli 1, 06123 Perugia, Italy; firstname.lastname@example.org
a3 Dipartimento di Matematica e Informatica, Università di Trieste, Via Valerio 12/1, 34127 Trieste, Italy; email@example.com
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)
Mathematics Subject Classification:
∗ 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.