A graphical representation of relational formulae with complementation

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

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 46 (2012) no. 2, pp. 261-289.

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.

Classification : 68Q40, 68T15, 03C10
Mots clés : algebra of binary relations, quantifier elimination, graph transformation

[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. | Zbl

[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. | Zbl

[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. | MR | Zbl

[6] S. Curtis and G. Lowe, Proofs with graphs. Sci. Comput. Program. 26 (1996) 197-216. | MR | Zbl

[7] R. De Freitas, P.A.S. Veloso, S.R.M. Veloso and P. Viana, On graph reasoning. Inf. Comput. 207 (2009) 228-246. | MR | Zbl

[8] N. Dershowitz and J.-P. Jouannaud, Rewrite systems, in Handbook of Theoretical Computer Science B : Formal Models and Semantics (B) (1990) 243-320. | MR | Zbl

[9] R.J. Duffin, Topology of series-parallel graphs. J. Math. Anal. Appl. 10 (1965) 303-318. | MR | Zbl

[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). | Zbl

[11] D. Dougherty and C. Gutiérrez, Normal forms for binary relations. Theoret. Comput. Sci. 360 (2006) 228-246. | MR | Zbl

[12] M.C. Fitting, First-order Logic and Automated Theorem Proving, Graduate Texts in Computer Science, 2nd edition. Springer-Verlag, New York (1996). | MR | Zbl

[13] A. Formisano and M. Nicolosi Asmundo, An efficient relational deductive system for propositional non-classical logics. JANCL 16 (2006) 367-408. | MR | Zbl

[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. | MR | Zbl

[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). | Zbl

[16] A. Formisano, E.G. Omodeo and M. Temperini, Goals and benchmarks for automated map reasoning. J. Symb. Comput. 29 (2000) 259-297. | MR | Zbl

[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). | MR | Zbl

[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. | Zbl

[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. | MR

[21] W. Kahl, Relational matching for graphical calculi of relations. Inform. Sci. 119 (1999) 253-273. | MR | Zbl

[22] M.K. Kwatinetz, Problems of expressibility in finite languages. Ph.D. thesis, University of California, Berkeley (1981). | MR

[23] R.M. Smullyan, First-order Logic. Dover Publications, New York (1995). | MR | Zbl

[24] A. Tarski and S. Givant, A formalization of Set Theory without variables, Amer. Math. Soc. Colloq. Publ. 41 (1987). | MR | Zbl

[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). | JFM