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.
@article{ITA_2012__46_2_261_0,
author = {Cantone, Domenico and Formisano, Andrea and Asmundo, Marianna Nicolosi and Omodeo, Eugenio Giovanni},
title = {A graphical representation of relational formulae with complementation},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
volume = {46},
year = {2012},
pages = {261-289},
doi = {10.1051/ita/2012003},
mrnumber = {2931249},
zbl = {1254.03020},
language = {en},
url = {http://dml.mathdoc.fr/item/ITA_2012__46_2_261_0}
}
Cantone, Domenico; Formisano, Andrea; Asmundo, Marianna Nicolosi; Omodeo, Eugenio Giovanni. A graphical representation of relational formulae with complementation. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 46 (2012) pp. 261-289. doi : 10.1051/ita/2012003. http://gdmltest.u-ga.fr/item/ITA_2012__46_2_261_0/
[1] , 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 0963.68183
[2] and , Categories, allegories and circuit design, in Proc. of 9th IEEE Symp. on Logic in Computer Science. IEEE Computer Society Press (1994) 372-381.
[3] and , Allegories of circuits, in Proc. of Logic for Computer Science (1994) 56-68. | Zbl 0964.94505
[4] , and , 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] , , and , Compiling dyadic first-order specifications into map algebra. Theoret. Comput. Sci. 293 (2003) 447-475. | MR 1964751 | Zbl 1025.68053
[6] and , Proofs with graphs. Sci. Comput. Program. 26 (1996) 197-216. | MR 1398233 | Zbl 0852.68070
[7] , , and , On graph reasoning. Inf. Comput. 207 (2009) 228-246. | MR 2921025 | Zbl 1187.68355
[8] and , Rewrite systems, in Handbook of Theoretical Computer Science B : Formal Models and Semantics (B) (1990) 243-320. | MR 1127191 | Zbl 0900.68283
[9] , Topology of series-parallel graphs. J. Math. Anal. Appl. 10 (1965) 303-318. | MR 175809 | Zbl 0128.37002
[10] and , 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 0964.03069
[11] and , Normal forms for binary relations. Theoret. Comput. Sci. 360 (2006) 228-246. | MR 2251226 | Zbl 1097.03059
[12] , First-order Logic and Automated Theorem Proving, Graduate Texts in Computer Science, 2nd edition. Springer-Verlag, New York (1996). | MR 1383320 | Zbl 0848.68101
[13] and , An efficient relational deductive system for propositional non-classical logics. JANCL 16 (2006) 367-408. | MR 2300567 | Zbl 1186.03044
[14] and , 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 1790850 | Zbl 0955.03016
[15] and , 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 1262.68078
[16] , and , Goals and benchmarks for automated map reasoning. J. Symb. Comput. 29 (2000) 259-297. | MR 1759961 | Zbl 0965.03014
[17] , and , 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] , and , Instructing equational set-reasoning with Otter, in Proc. of IJCAR'01, edited by R. Goré, A. Leitsch and T. Nipkow (2001). | MR 2049507 | Zbl 0988.68164
[19] , and , 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 1263.03008
[20] , 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 1478226
[21] , Relational matching for graphical calculi of relations. Inform. Sci. 119 (1999) 253-273. | MR 1729775 | Zbl 0943.68092
[22] , Problems of expressibility in finite languages. Ph.D. thesis, University of California, Berkeley (1981). | MR 2631520
[23] , First-order Logic. Dover Publications, New York (1995). | MR 1314201 | Zbl 0172.28901
[24] and , A formalization of Set Theory without variables, Amer. Math. Soc. Colloq. Publ. 41 (1987). | MR 920815 | Zbl 0654.03036
[25] , 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 51.0163.04