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

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 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
  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.  
  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.  
  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.  
  6. S. Curtis and G. Lowe, Proofs with graphs. Sci. Comput. Program.26 (1996) 197–216.  
  7. R. de Freitas, P.A.S. Veloso, S.R.M. Veloso and P. Viana, On graph reasoning. Inf. Comput.207 (2009) 228–246.  
  8. N. Dershowitz and J.-P. Jouannaud, Rewrite systems, in Handbook of Theoretical Computer Science B : Formal Models and Semantics (B) (1990) 243–320.  
  9. R.J. Duffin, Topology of series-parallel graphs. J. Math. Anal. Appl.10 (1965) 303–318.  
  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).  
  11. D. Dougherty and C. Gutiérrez, Normal forms for binary relations. Theoret. Comput. Sci.360 (2006) 228–246.  
  12. M.C. Fitting, First-order Logic and Automated Theorem Proving, Graduate Texts in Computer Science, 2nd edition. Springer-Verlag, New York (1996).  
  13. A. Formisano and M. Nicolosi Asmundo, An efficient relational deductive system for propositional non-classical logics. JANCL16 (2006) 367–408.  
  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.  
  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).  
  16. A. Formisano, E.G. Omodeo and M. Temperini, Goals and benchmarks for automated map reasoning. J. Symb. Comput.29 (2000) 259–297.  
  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).  
  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.  
  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.  
  21. W. Kahl, Relational matching for graphical calculi of relations. Inform. Sci.119 (1999) 253–273.  
  22. M.K. Kwatinetz, Problems of expressibility in finite languages. Ph.D. thesis, University of California, Berkeley (1981).  
  23. R.M. Smullyan, First-order Logic. Dover Publications, New York (1995).  
  24. A. Tarski and S. Givant, A formalization of Set Theory without variables, Amer. Math. Soc. Colloq. Publ.41 (1987).  
  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).  

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.