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

Abstract

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

How to cite

top

Cantone, 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. [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. [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. [3] C. Brown and A. Jeffrey, Allegories of circuits, in Proc. of Logic for Computer Science (1994) 56–68. Zbl0964.94505
  4. [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. [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. [6] S. Curtis and G. Lowe, Proofs with graphs. Sci. Comput. Program.26 (1996) 197–216. Zbl0852.68070MR1398233
  7. [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. [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. [9] R.J. Duffin, Topology of series-parallel graphs. J. Math. Anal. Appl.10 (1965) 303–318. Zbl0128.37002MR175809
  10. [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. [11] D. Dougherty and C. Gutiérrez, Normal forms for binary relations. Theoret. Comput. Sci.360 (2006) 228–246. Zbl1097.03059MR2251226
  12. [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. [13] A. Formisano and M. Nicolosi Asmundo, An efficient relational deductive system for propositional non-classical logics. JANCL16 (2006) 367–408. Zbl1186.03044MR2300567
  14. [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. [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. [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. [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. [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. [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. [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. [21] W. Kahl, Relational matching for graphical calculi of relations. Inform. Sci.119 (1999) 253–273. Zbl0943.68092MR1729775
  22. [22] M.K. Kwatinetz, Problems of expressibility in finite languages. Ph.D. thesis, University of California, Berkeley (1981). MR2631520
  23. [23] R.M. Smullyan, First-order Logic. Dover Publications, New York (1995). Zbl0172.28901MR1314201
  24. [24] A. Tarski and S. Givant, A formalization of Set Theory without variables, Amer. Math. Soc. Colloq. Publ. 41 (1987). Zbl0654.03036MR920815
  25. [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 ?

top

You must be logged in to post comments.

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

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.