Advertisement

Reasoning on Relations, Modalities, and Sets

  • Andrea Formisano
  • Eugenio G. Omodeo
  • Alberto Policriti
Chapter
Part of the Outstanding Contributions to Logic book series (OCTR, volume 17)

Abstract

This survey discusses the interplay among unquantified relational logics, propositional modal logics, and set theories. To set up a common ground, cross-translation methods among languages commonly used to work with relations, modalities, and sets, are revisited. This paper also reports on many experiments aimed at providing automated support for reasoning based on the calculus of dyadic relations.

Keywords

Modal translation methods Set-theoretic deduction Automated equational reasoning Relation algebras Algebraic logic Pairing 

Notes

Acknowledgements

The authors are grateful to the anonymous referees for careful reading and providing invaluable advice: one of them even produced a detailed sketch of the proof of Lemma 6.3 and showed that it must rely on (E). Thanks are also due to Giovanna D’Agostino for pleasant discussions, concerning in particular Sect. 6.2.

References

  1. Aczel, P. (1988). Non-well-founded Sets. CSLI Lecture Notes.Google Scholar
  2. Bresolin, D., Golińska-Pilarek, J., & Orłowska, E. (2006). A relational dual tableaux for interval temporal logics. Journal of Applied Non-classical Logics, 16(3–4), 251–278.CrossRefGoogle Scholar
  3. Brink, C., Kahl, W., & Schmidt, G. (Eds.). (1997). Relational Methods in Computer Science. Advances in Computing Science. New York: Springer.Google Scholar
  4. Burrieza, A., Mora, A., Ojeda-Aciego, M., & Orłowska, E. (2009). An implementation of a dual tableaux system for order-of-magnitude qualitative reasoning. International Journal of Computer Mathematics, 86(10–11), 1852–1866.CrossRefGoogle Scholar
  5. Caianiello, P., Costantini, S., & Omodeo, E. G. (2003). An environment for specifying properties of dyadic relations and reasoning about them I: Language extension mechanisms. In H. de Swart, E. Orłowska, M. Roubens, & G. Schmidt (Eds.), Theory and Applications of Relational Structures as Knowledge Instruments (Vol. 2929, pp. 87– 106). Lecture Notes in Computer Science. Berlin: Springer.Google Scholar
  6. Cantone, D., Cavarra, A., & Omodeo, E. (1997). On existentially quantified conjunctions of atomic formulae of \({\mathscr {L}^+}\). In M. P. Bonacina & U. Furbach (Eds.), Proceedings of the FTP97 International Workshop on First-Order Theorem Proving (97–50, pp. 45–52). RISC-Linz Report Series.Google Scholar
  7. Cantone, D., Omodeo, E., & Policriti, A. (2001). Set Theory for Computing–From Decision Procedures to Declarative Programming with Sets. Monographs in Computer Science. Berlin: Springer.Google Scholar
  8. Cantone, D., Formisano, A., Omodeo, E., & Zarba, C. G. (2003). Compiling dyadic first-order specifications into map algebra. Theoretical Computer Science, 293(2), 447–475.CrossRefGoogle Scholar
  9. Cantone, D., Formisano, A., Nicolosi Asmundo, M., & Omodeo, E. (2012). A graphical representation of relational formulae with complementation. RAIRO – Theoretical Informatics and Applications, 46(2), 261–289.CrossRefGoogle Scholar
  10. Cohen, P. J. (1966). Set Theory and the Continuum Hypothesis. New York: Benjamin.Google Scholar
  11. D’Agostino, G., Montanari, A., & Policriti, A. (1995). A set-theoretic translation method for polymodal logics. Journal of Automated Reasoning, 15(3), 317–337.CrossRefGoogle Scholar
  12. Demri, S. & Orłowska, E. (1996). Logical analysis of demonic nondeterministic programs. Theoretical Computer Science, 166(1–2), 173–202.CrossRefGoogle Scholar
  13. Demri, S. & Orłowska, E. (2002). Incomplete Information: Structure, Inference, Complexity. Monographs in Theoretical Computer Science. An EATCS series. Berlin: Springer.CrossRefGoogle Scholar
  14. Dovier, A., Formisano, A., & Omodeo, E. (2006). Decidability results for sets with atoms. ACM Transactions on Computational Logic, 7(2), 269–301.CrossRefGoogle Scholar
  15. Düntsch, I. & Orłowska, E. (2001). Beyond modalities: Sufficiency and mixed algebras. In E. Orłowska & A. Szałas (Eds.), Relational Methods for Computer Science Applications (Vol. 65, pp. 263–285). Studies in Fuzziness and Soft Computing. Heidelberg: Springer-Physica Verlag.CrossRefGoogle Scholar
  16. Düntsch, I. & Orłowska, E. (2000). Logics of complementarity in information systems. Mathematical Logic Quarterly, 46(2), 267–288.CrossRefGoogle Scholar
  17. Düntsch, I., Orłowska, E., Radzikowska, A., & Vakarelov, D. (2005). Relational representation theorems for some lattice-based structures. Journal of Relational Methods in Computer Science, 1, 132–160.Google Scholar
  18. Formisano, A. & Omodeo, E. (2000). An equational re-engineering of set theories. In R. Caferra & G. Salzer (Eds.), Automated Deduction in Classical and Nonclassical Logics, Selected Papers (Vol. 1761, pp. 175–190). Lecture Notes in Computer Science. Berlin: Springer.CrossRefGoogle Scholar
  19. Formisano, A. & Nicolosi Asmundo, M. (2006). An efficient relational deductive system for propositional non-classical logics. Journal of Applied Non-Classical Logics, 16(3–4), 367–408.CrossRefGoogle Scholar
  20. Formisano, A. & Simeoni, M. (2001). An AGG application supporting visual reasoning. Electronic Notes in Theoretical Computer Science, 50(3), 302–309.CrossRefGoogle Scholar
  21. Formisano, A., Omodeo, E., & Temperini, M. (2000). Goals and benchmarks for automated map reasoning. Journal of Symbolic Computation, 29(2), 259–297.CrossRefGoogle Scholar
  22. Formisano, A., Omodeo, E., & Simeoni, M. (2001a). A graphical approach to relational reasoning. Electronic Notes in Theoretical Computer Science, 44(3), 153–174.Google Scholar
  23. Formisano, A., Omodeo, E., & Temperini, M. (2001b). Layered map reasoning: An experimental approach put to trial on sets. Electronic Notes in Theoretical Computer Science, 48, 1–28.CrossRefGoogle Scholar
  24. Formisano, A., Omodeo, E., & Temperini, M. (2001c). Instructing equational setreasoning with Otter. In R. Goré, A. Leitsch, & T. Nipkow (Eds.), Automated Reasoning, Proceedings of the 1st International Joint Conference, IJCAR 2001 (Vol. 2083, pp. 152–167). Lecture Notes in Computer Science. Berlin: Springer.CrossRefGoogle Scholar
  25. Formisano, A., Omodeo, E., & Policriti, A. (2004). Three-variable statements of set-pairing. Theoretical Computer Science, 322(1), 147–173.CrossRefGoogle Scholar
  26. Formisano, A., Omodeo, E., & Policriti, A. (2005). The axiom of elementary sets on the edge of Peircean expressibility. Journal of Symbolic Logic, 70(3), 953–968.CrossRefGoogle Scholar
  27. Formisano, A., Omodeo, E., & Orłowska, E. (2006). An environment for specifying properties of dyadic relations and reasoning about them II: Relational presentation of non-classical logics. In H. de Swart, E. Orłowska, M. Roubens, & G. Schmidt (Eds.), Theory and Applications of Relational Structures as Knowledge Instruments II: International Workshops of COST Action 274, TARSKI, 2002–2005, Selected Revised Papers (Vol. 4342, pp. 89–104). Lecture Notes in Artificial Intelligence. Berlin: Springer.CrossRefGoogle Scholar
  28. Golińska-Pilarek, J. & Orłowska, E. (2007). Tableaux and dual tableaux: Transformation of proofs. Studia Logica, 85(3), 283–302.CrossRefGoogle Scholar
  29. Golińska-Pilarek, J. & Orłowska, E. (2011). Dual tableau for monoidal triangular norm logic MTL. Fuzzy Sets and Systems, 162(1), 39–52.CrossRefGoogle Scholar
  30. Goranko, V. (1990). Modal definability in enriched languages. Notre Dame Journal of Formal Logic, 31(1), 81–105.CrossRefGoogle Scholar
  31. Humberstone, L. (1983). Inaccessible worlds. Notre Dame Journal of Formal Logic, 24(3), 346–352.CrossRefGoogle Scholar
  32. Järvinen, J. & Orłowska, E. (2006). Relational correspondences for lattices with operators. In W. MacCaull, M. Winter, & I. Düntsch (Eds.), Relational Methods in Computer Science: 8th International Seminar on Relational Methods in Computer Science, 3rd International Workshop on Applications of Kleene Algebra, and Workshop of COST Action 274: TARSKI, Selected Revised Papers (Vol. 3929, pp. 134–146). Lecture Notes in Computer Science. Berlin: Springer.CrossRefGoogle Scholar
  33. Jech, T. J. (1978). Set Theory. New York: Academic Press.Google Scholar
  34. Jifeng, H. & Hoare, C. A. R. (1986). Weakest prespecifications, Part I. Fundamenta Informaticae, 9, 51–84. Part II: ibidem, 9, 217–252.Google Scholar
  35. Konikowska, B., Morgan, C., & Orłowska, E. (1998). A relational formalisation of arbitrary finite-valued logics. Logic Journal of the IGPL, 6(5), 755–774.CrossRefGoogle Scholar
  36. Kwatinetz, M. K. (1981). Problems of Expressibility in Finite Languages. Doctoral dissertation, University of California, Berkeley.Google Scholar
  37. MacCaull, W. & Orłowska, E. (2002). Correspondence results for relational proof systems with applications to the Lambek calculus. Studia Logica, 71(3), 389–414.CrossRefGoogle Scholar
  38. MacCaull, W. & Orłowska, E. (2006). A logic of typed relations and its applications to relational databases. Journal of Logic and Computation, 16(6), 789–815.CrossRefGoogle Scholar
  39. Maddux, R. D. (2006). Relation Algebras. Studies in Logic and the Foundations of Mathematics. Amsterdam: Elsevier.Google Scholar
  40. Manin, Y. I. (2010). A Course in Mathematical Logic for Mathematicians (2nd ed.). Graduate Texts in Mathematics. Berlin: Springer.CrossRefGoogle Scholar
  41. McCune, W. W. (2003). OTTER 3.3 reference manual. CoRR, arXiv:cs.SC/0310056. Retrieved from http://arxiv.org/abs/cs.SC/0310056.
  42. McCune, W. W. (2005–2010). Prover9 and Mace4. http://www.cs.unm.edu/~mccune/prover9/.
  43. Omodeo, E., Orłowska, E., & Policriti, A. (2004). Rasiowa-Sikorski style relational elementary set theory. In R. Berghammer, B. Möller, & G. Struth (Eds.), Relational and Kleene-Algebraic Methods in Computer Science: 7th International Seminar on Relational Methods in Computer Science and 2nd International Workshop on Applications of Kleene Algebra, Bad Malente, Germany, May 12–17, 2003, Revised Selected Papers (Vol. 3051, pp. 215–226). Lecture Notes in Computer Science. Berlin: Springer.Google Scholar
  44. Omodeo, E., Policriti, A., & Tomescu, A. I. (2012). Infinity, in short. Journal of Logic and Computation, 22(6), 1391–1403.CrossRefGoogle Scholar
  45. Orłowska, E. (1988a). Proof system for weakest prespecification. Information Processing Letters, 27(6), 309–313.CrossRefGoogle Scholar
  46. Orłowska, E. (1988b). Relational interpretation of modal logics. In H. Andreka, D. Monk, & I. Németi (Eds.), Algebraic Logic. Colloquia Mathematica Societatis Janos Bolyai (Vol. 54, pp. 443–471). Amsterdam: North Holland.Google Scholar
  47. Orłowska, E. (1992). Relational proof systems for relevant logics. Journal of Symbolic Logic, 57(4), 1425–1440.CrossRefGoogle Scholar
  48. Orłowska, E. (1994). Relational semantics for non-classical logics: Formulas are relations. In J. Woleński (Ed.), Philosophical Logic in Poland (pp. 167–186). New York: Kluwer.CrossRefGoogle Scholar
  49. Orłowska, E. (1995). Temporal logics in a relational framework. In L. Bolc & A. Szałas (Eds.), Time and Logic: a Computational Approach (pp. 249–277). University College London Press.Google Scholar
  50. Orłowska, E. (1996). Relational proof systems for modal logics. In H. Wansing (Ed.), Proof Theory of Modal Logics (pp. 55–78). Berlin-New York: Kluwer Academic Publishers.Google Scholar
  51. Orłowska, E. (1997). Relational formalisation of nonclassical logics. In C. Brink, W. Kahl, & G. Schmidt (Eds.), Relational Methods in Computer Science (pp. 90–105). Wien/New York: Springer.CrossRefGoogle Scholar
  52. Orłowska, E. & Golińska-Pilarek, J. (2011). Dual Tableaux: Foundations, Methodology, Case Studies. Trends in Logic. Dordrecht-Heidelberg-London-New York: Springer.CrossRefGoogle Scholar
  53. Orłowska, E. & Vakarelov, D. (2005). Lattice-based modal algebras and modal logics. In P. Hájek, L. Valdés-Villanueva, & D. Westerståhl (Eds.), Logic, Methodology and Philosophy of Science: Proceedings of the 12th International Congress (pp. 147–170). Abstract in the volume of abstracts, 22–23. King’s College London Publications.Google Scholar
  54. Parlamento, F. & Policriti, A. (1991). Expressing infinity without foundation. Journal of Symbolic Logic, 56(4), 1230–1235.CrossRefGoogle Scholar
  55. Paulson, L. C. & Grąbczewski, K. (1996). Mechanizing set theory. Journal of Automated Reasoning, 17(3), 291–323.Google Scholar
  56. Rasiowa, H. & Sikorski, R. (1963). The Mathematics of Metamathematics. Warsaw: Polish Scientific Publishers.Google Scholar
  57. Schmidt, G. (2011). Relational Mathematics. Encyclopedia of Mathematics and its Applications. Cambridge: Cambridge University Press.Google Scholar
  58. Schmidt, G. & Ströhlein, T. (1993). Relations and Graphs, Discrete Mathematics for Computer Scientists. EATCS Monographs on Theoretical Computer Science. Berlin: Springer.Google Scholar
  59. Tarski, A. (1953a). A formalization of set theory without variables. Journal of Symbolic Logic, 18, 189 (Abstracts of the 15th meeting of the Association for Symbolic Logic).Google Scholar
  60. Tarski, A. (1953b). Some metalogical results concerning the calculus of relations. Journal of Symbolic Logic, 18, 188–189 (Abstracts of the 15th meeting of the Association for Symbolic Logic).Google Scholar
  61. Tarski, A. & Givant, S. (1987). Formalization of Set Theory Without Variables. Colloquium Publications. Providence: American Mathematical Society.Google Scholar
  62. van Benthem, J., D’Agostino, G., Montanari, A., & Policriti, A. (1996). Modal deduction in second-order logic and set theory-I. Journal of Logic and Computation, 7(2), 251–265.CrossRefGoogle Scholar
  63. van Benthem, J., D’Agostino, G., Montanari, A., & Policriti, A. (1998). Modal deduction in second-order logic and set theory-II. Studia Logica, 60(2), 387–420.CrossRefGoogle Scholar
  64. Zermelo, E. (1977). Untersuchungen über die Grundlagen der Mengenlehre I. In J. Van Heijenoort (Ed.), From Frege to Gödel – A Source Book in Mathematical Logic, 1879–1931 (3rd edn., pp. 199–215). Cambridge: Harvard University Press.Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Andrea Formisano
    • 1
  • Eugenio G. Omodeo
    • 2
  • Alberto Policriti
    • 3
  1. 1.Dipartimento di Matematica e InformaticaUniversità di PerugiaPerugiaItaly
  2. 2.Dipartimento di Matematica e GeoscienzeUniversità di TriesteTriesteItaly
  3. 3.Dipartimento di Scienze Matematiche, Informatiche e FisicheUniversità di UdineUdineItaly

Personalised recommendations