# A graphical representation of relational formulae with complementation

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

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et 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 - Informatique Théorique et Applications 46.2 (2012): 261-289. <http://eudml.org/doc/273061>.

@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 - Informatique Théorique et Applications},

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

language = {eng},

number = {2},

pages = {261-289},

publisher = {EDP-Sciences},

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

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

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 - Informatique Théorique et Applications

PY - 2012

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; dyadic first-order sentences; translation techniques; graphical representation of formulae; relational complement

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

ER -

## References

top- [1] 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
- [2] 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.
- [3] C. Brown and A. Jeffrey, Allegories of circuits, in Proc. of Logic for Computer Science (1994) 56–68. Zbl0964.94505
- [4] 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).
- [5] 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.68053MR1964751
- [6] S. Curtis and G. Lowe, Proofs with graphs. Sci. Comput. Program.26 (1996) 197–216. Zbl0852.68070MR1398233
- [7] R. de Freitas, P.A.S. Veloso, S.R.M. Veloso and P. Viana, On graph reasoning. Inf. Comput.207 (2009) 228–246. Zbl1187.68355MR2921025
- [8] N. Dershowitz and J.-P. Jouannaud, Rewrite systems, in Handbook of Theoretical Computer Science B : Formal Models and Semantics (B) (1990) 243–320. Zbl0900.68283MR1127191
- [9] R.J. Duffin, Topology of series-parallel graphs. J. Math. Anal. Appl.10 (1965) 303–318. Zbl0128.37002MR175809
- [10] 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
- [11] D. Dougherty and C. Gutiérrez, Normal forms for binary relations. Theoret. Comput. Sci.360 (2006) 228–246. Zbl1097.03059MR2251226
- [12] M.C. Fitting, First-order Logic and Automated Theorem Proving, Graduate Texts in Computer Science, 2nd edition. Springer-Verlag, New York (1996). Zbl0848.68101MR1383320
- [13] A. Formisano and M. Nicolosi Asmundo, An efficient relational deductive system for propositional non-classical logics. JANCL16 (2006) 367–408. Zbl1186.03044MR2300567
- [14] 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.03016MR1790850
- [15] 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
- [16] A. Formisano, E.G. Omodeo and M. Temperini, Goals and benchmarks for automated map reasoning. J. Symb. Comput.29 (2000) 259–297. Zbl0965.03014MR1759961
- [17] 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).
- [18] 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.68164MR2049507
- [19] 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
- [20] 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. MR1478226
- [21] W. Kahl, Relational matching for graphical calculi of relations. Inform. Sci.119 (1999) 253–273. Zbl0943.68092MR1729775
- [22] M.K. Kwatinetz, Problems of expressibility in finite languages. Ph.D. thesis, University of California, Berkeley (1981). MR2631520
- [23] R.M. Smullyan, First-order Logic. Dover Publications, New York (1995). Zbl0172.28901MR1314201
- [24] A. Tarski and S. Givant, A formalization of Set Theory without variables, Amer. Math. Soc. Colloq. Publ. 41 (1987). Zbl0654.03036MR920815
- [25] 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). JFM51.0163.04

## NotesEmbed ?

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