# A graphical representation of relational formulae with complementation∗

Domenico Cantone; Andrea Formisano; Marianna Nicolosi Asmundo; Eugenio Giovanni Omodeo

RAIRO - Theoretical Informatics and Applications (2012)

- Volume: 46, Issue: 2, page 261-289
- ISSN: 0988-3754

## Access Full Article

top## Abstract

top## How to cite

topCantone, Domenico, et al. "A graphical representation of relational formulae with complementation∗." RAIRO - Theoretical Informatics and Applications 46.2 (2012): 261-289. <http://eudml.org/doc/222034>.

@article{Cantone2012,

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.},

author = {Cantone, Domenico, Formisano, Andrea, Asmundo, Marianna Nicolosi, Omodeo, Eugenio Giovanni},

journal = {RAIRO - Theoretical Informatics and Applications},

keywords = {Algebra of binary relations; quantifier elimination; graph transformation; algebra of binary relations; dyadic first-order sentences; translation techniques; graphical representation of formulae; relational complement},

language = {eng},

month = {4},

number = {2},

pages = {261-289},

publisher = {EDP Sciences},

title = {A graphical representation of relational formulae with complementation∗},

url = {http://eudml.org/doc/222034},

volume = {46},

year = {2012},

}

TY - JOUR

AU - Cantone, Domenico

AU - Formisano, Andrea

AU - Asmundo, Marianna Nicolosi

AU - Omodeo, Eugenio Giovanni

TI - A graphical representation of relational formulae with complementation∗

JO - RAIRO - Theoretical Informatics and Applications

DA - 2012/4//

PB - EDP Sciences

VL - 46

IS - 2

SP - 261

EP - 289

AB - 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.

LA - eng

KW - Algebra of binary relations; quantifier elimination; graph transformation; algebra of binary relations; dyadic first-order sentences; translation techniques; graphical representation of formulae; relational complement

UR - http://eudml.org/doc/222034

ER -

## References

top- J.G.F. Belinfante, Gödel’s algorithm for class formation, in Proc. of CADE’00, edited by D. McAllester. Lect. Notes Comput. Sci.1831 (2000) 132–147. Zbl0963.68183
- C. Brown and G. Hutton, Categories, allegories and circuit design, in Proc. of 9th IEEE Symp. on Logic in Computer Science. IEEE Computer Society Press (1994) 372–381.
- C. Brown and A. Jeffrey, Allegories of circuits, in Proc. of Logic for Computer Science (1994) 56–68. Zbl0964.94505
- D. Cantone, A. Cavarra and E.G. Omodeo, On existentially quantified conjunctions of atomic formulae of ℒ+, in Proc. of International Workshop on First-Order Theorem Proving (FTP97), edited by M.P. Bonacina and U. Furbach (1997).
- D. Cantone, A. Formisano, E.G. Omodeo and C.G. Zarba, Compiling dyadic first-order specifications into map algebra. Theoret. Comput. Sci.293 (2003) 447–475. Zbl1025.68053
- S. Curtis and G. Lowe, Proofs with graphs. Sci. Comput. Program.26 (1996) 197–216. Zbl0852.68070
- R. de Freitas, P.A.S. Veloso, S.R.M. Veloso and P. Viana, On graph reasoning. Inf. Comput.207 (2009) 228–246. Zbl1187.68355
- N. Dershowitz and J.-P. Jouannaud, Rewrite systems, in Handbook of Theoretical Computer Science B : Formal Models and Semantics (B) (1990) 243–320. Zbl0900.68283
- R.J. Duffin, Topology of series-parallel graphs. J. Math. Anal. Appl.10 (1965) 303–318. Zbl0128.37002
- D. Dougherty and C. Gutiérrez, Normal forms and reduction for theories of binary relations, in Proc. of Rewriting Techniques and Applications, edited by L. Bachmair. Lect. Notes Comput. Sci.1833 (2000). Zbl0964.03069
- D. Dougherty and C. Gutiérrez, Normal forms for binary relations. Theoret. Comput. Sci.360 (2006) 228–246. Zbl1097.03059
- M.C. Fitting, First-order Logic and Automated Theorem Proving, Graduate Texts in Computer Science, 2nd edition. Springer-Verlag, New York (1996).
- A. Formisano and M. Nicolosi Asmundo, An efficient relational deductive system for propositional non-classical logics. JANCL16 (2006) 367–408. Zbl1186.03044
- A. Formisano and E.G. Omodeo, An equational re-engineering of set theories, in Selected Papers from Automated Deduction in Classical and Non-Classical Logics, edited by R. Caferra and G. Salzer. Lect. Notes Comput. Sci.1761 (2000) 175–190. Zbl0955.03016
- A. Formisano and M. Simeoni, An Agg application supporting visual reasoning, in Proc. of GT-VMT’01 (ICALP 2001), edited by L. Baresi and M. Pezzè. Electron. Notes Theoret. Comput. Sci.50 (2001). Zbl1262.68078
- A. Formisano, E.G. Omodeo and M. Temperini, Goals and benchmarks for automated map reasoning. J. Symb. Comput.29 (2000) 259–297. Zbl0965.03014
- A. Formisano, E.G. Omodeo and M. Simeoni, A graphical approach to relational reasoning, in Proc. of RelMiS 2001 (ETAPS 2001), edited by W. Kahl, D.L. Parnas and G. Schmidt. Electron. Notes Theoret. Comput. Sci.44 (2001).
- A. Formisano, E.G. Omodeo and M. Temperini, Instructing equational set-reasoning with Otter, in Proc. of IJCAR’01, edited by R. Goré, A. Leitsch and T. Nipkow (2001). Zbl0988.68164
- A. Formisano, E.G. Omodeo and M. Temperini, Layered map reasoning : An experimental approach put to trial on sets, in Declarative Programming, edited by A. Dovier, M.-C. Meo and A. Omicini. Electron. Notes Theoret. Comput. Sci.48 (2001) 1–28. Zbl1263.03008
- W. Kahl, Algebraic graph derivations for graphical calculi, in Proc. of Graph Theoretic Concepts in Computer Science, WG ’96, edited by F. d’Amore, P.G. Franciosa and A. Marchetti-Spaccamela. Lect. Notes Comput. Sci.1197 (1997) 224–238.
- W. Kahl, Relational matching for graphical calculi of relations. Inform. Sci.119 (1999) 253–273. Zbl0943.68092
- M.K. Kwatinetz, Problems of expressibility in finite languages. Ph.D. thesis, University of California, Berkeley (1981).
- R.M. Smullyan, First-order Logic. Dover Publications, New York (1995). Zbl0172.28901
- A. Tarski and S. Givant, A formalization of Set Theory without variables, Amer. Math. Soc. Colloq. Publ.41 (1987). Zbl0654.03036
- J. von Neumann, Eine Axiomatisierung der Mengenlehre. J. Reine Angew. Math.154 (1925) 219–240. English translation, edited by J. van Heijenoort. From Frege to Gödel : a source book in mathematical logic, 1879–1931. Harvard University Press (1977).

## NotesEmbed ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.