Skip to main content
SpringerLink
Log in

An Environment for Specifying Properties of Dyadic Relations and Reasoning About Them II: Relational Presentation of Non-classical Logics

  • Conference paper
Theory and Applications of Relational Structures as Knowledge Instruments II

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 4342))

Abstract

This paper contributes to the vast literature on relational renderings of non-classical logics providing a general schema for automatic translation. The translation process is supported by a flexible Prolog tool. Many specific translations are already implemented, typically leading from an unquantified logic into the calculus of binary relations. Thanks to the uniformity of the translation pattern, additional source languages (and, though less commonly, new target languages) can be installed very easily into this Prolog-based translator. The system also integrates an elementary graphical proof assistant based on Rasiowa-Sikorski dual-tableau rules.

Research partially funded by INTAS project Algebraic and deduction methods in non-classical logic and their applications to Computer Science, and by the European Concerted Research Action COST 274, TARSKI: Theory and Applications of Relational Structures as Knowledge Instruments.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. van Benthem, J.F.A.K., D’Agostino, G., Montanari, A., Policriti, A.: Modal deduction in second-order logic and set theory-I. Journal of Logic and Computation 7(2), 251–265 (1997)

    Article  MATH  MathSciNet  Google Scholar 

  2. Cantone, D., Formisano, A., Omodeo, E.G., Zarba, C.G.: Compiling dyadic first-order specifications into map algebra. Theoretical Computer Science 293(2), 447–475 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  3. Caianiello, P., Costantini, S., Omodeo, E.G.: An Environment for Specifying Properties of Dyadic Relations and Reasoning about Them. I: Language Extension Mechanisms. In: de Swart, H., Orłowska, E., Schmidt, G., Roubens, M. (eds.) Theory and Applications of Relational Structures as Knowledge Instruments. LNCS, vol. 2929, pp. 87–106. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  4. D’Agostino, G., Montanari, A., Policriti, A.: A set-theoretic translation method for polymodal logics. Journal of Automated Reasoning 3(15), 317–337 (1995)

    Article  MathSciNet  Google Scholar 

  5. Demri, S., Orłowska, E.: Incomplete Information: Structure, Inference, Complexity. EATCS Monographs in Theoretical Computer Science. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  6. Düntsch, I., Orłowska, E.: Beyond modalities: sufficiency and mixed algebras. In: Orłowska, E., Szalas, A. (eds.) Relational Methods in Computer Science Applications, pp. 277–299. Physica-Verlag, Heidelberg (2000)

    Google Scholar 

  7. Düntsch, I., Orłowska, E., Radzikowska, A.M., Vakarelov, D.: Relational Representation Theorems for Some Lattice-Based Structures. Journal on Relational Methods in Computer Science 1, 132–160 (2004)

    Google Scholar 

  8. Formisano, A., Nicolosi Asmundo, M.: An efficient relational deductive system for propositional non-classical logics. Journal of Applied Non-Classical Logics (to appear) (A draft version is available as report 8/06 of the Dipartimento di Informatica, Università di L’Aquila, 2006)

    Google Scholar 

  9. Formisano, A., Omodeo, E., Orłowska, E., Policriti, A.: Uniform relational frameworks for modal inferences. In: Düntsch, I., Winter, M. (eds.) Proceedings of the 8th International Conference on Relational Methods in Computer Science (RelMiCS 8) (2005)

    Google Scholar 

  10. Formisano, A., Omodeo, E., Simeoni, M.: A graphical approach to relational reasoning. Electronic Notes in Theoretical Computer Science, vol. 44(3). Elsevier, Amsterdam (2001)

    Google Scholar 

  11. Formisano, A., Omodeo, E.G., Temperini, M.: Instructing Equational Set-Reasoning with Otter. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS, vol. 2083, pp. 152–167. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  12. Formisano, A., Omodeo, E.G., Temperini, M.: Layered map reasoning: An experimental approach put to trial on sets. Electronic Notes in Theoretical Computer Science, vol. 48. Elsevier, Amsterdam (2001)

    Google Scholar 

  13. Formisano, A., Policriti, A.: T-Resolution: Refinements and Model Elimination. Journal of Automated Reasoning 22(4), 433–483 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  14. Frias, M., Orłowska, E.: Equational reasoning in nonclassical logics. Journal of Applied Non-Classical Logics 8(1-2), 27–66 (1998)

    MATH  MathSciNet  Google Scholar 

  15. Goranko, V.: Modal definability in enriched languages. Notre Dame Journal of Formal Logic 31, 81–105 (1990)

    Article  MATH  MathSciNet  Google Scholar 

  16. Goré, R.: Cut-free display calculi for relation algebras. In: van Dalen, D., Bezem, M. (eds.) CSL 1996. LNCS, vol. 1258, pp. 198–210. Springer, Heidelberg (1997)

    Google Scholar 

  17. Hennessy, M.C.B.: A proof system for the first order relational calculus. Journal of Computer and System Sciences 20, 96–110 (1980)

    Article  MATH  MathSciNet  Google Scholar 

  18. Hoare, C.A.R., Jifeng, H.: The weakest prespecification. Fundamenta Informaticae IX, 51–84, Part II ibidem IX, 217–252 (1986)

    Google Scholar 

  19. Humberstone, I.L.: Inaccessible worlds. Notre Dame Journal of Formal Logic 24, 346–352 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  20. Järvinen, J., Orłowska, E.: Relational correspondences for lattices with operators. In: MacCaull, W., Winter, M., Düntsch, I. (eds.) RelMiCS 2005. LNCS, vol. 3929, pp. 111–118. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  21. Kwatinetz, M.K.: Problems of expressibility in finite languages. PhD thesis, University of California, Berkeley (1981)

    Google Scholar 

  22. Maddux, R.: A sequent calculus for relation algebras. Annals of Pure and Applied Logic 25, 73–101 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  23. Ohlbach, H.J., Nonnengart, A., de Rijke, M., Gabbay, D.: Encoding Two-Valued Nonclassical Logics in Classical Logic. In: Handbook of Automated Reasoning, vol. II, pp. 1403–1486. Elsevier, Amsterdam (2001)

    Chapter  Google Scholar 

  24. Orłowska, E.: Proof system for weakest prespecification. Information Processing Letters 27, 309–313 (1988)

    Article  MATH  MathSciNet  Google Scholar 

  25. Orłowska, E.: Relational interpretation of modal logics. In: Andreka, H., Monk, D., Nemeti, I. (eds.) Algebraic Logic. Colloquia Mathematica Societatis Janos Bolyai, vol. 54, pp. 443–471. North Holland, Amsterdam (1998)

    Google Scholar 

  26. Orłowska, E.: Relational proof systems for relevant logics. Journal of Symbolic Logic 57, 167–186 (1992)

    Google Scholar 

  27. Orłowska, E.: Relational semantics for nonclassical logics: formulas are relations. In: Wolenski, J. (ed.) Philosophical Logic in Poland, pp. 167–186. Kluwer, Dordrecht (1994)

    Google Scholar 

  28. Orłowska, E.: Temporal logics in a relational framework. Time and Logic—A computational Approach, pp. 227–249. University College London Press (1995)

    Google Scholar 

  29. Orłowska, E.: Relational proof systems for modal logics. In: Wansing, H. (ed.) Proof theory of modal logic. Applied logic series, vol. 2, pp. 55–78. Kluwer, Dordrecht (1996)

    Google Scholar 

  30. Orłowska, E.: Relational formalization of nonclassical logics. In: Brink, C., Kahl, W., Schmidt, G. (eds.) Relational Methods in Computer Science, pp. 90–105. Springer, Heidelberg (1997)

    Google Scholar 

  31. Omodeo, E.G., Orłowska, E., Policriti, A.: Rasiowa-Sikorski style relational elementary set theory. In: Berghammer, R., Moeller, B. (eds.) Proceedings 7th International Conference on Relational Methods in Computer Science (RelMiCS 7) LNCS, vol. 3051, pp. 215–226. Springer, Heidelberg (2003)

    Google Scholar 

  32. Orłowska, E., Vakarelov, D.: Lattice-based modal algebras and modal logics. In: Hajek, P., Valdés-Villanueva, L.M., Westerstahl, D. (eds.) Logic, Methodology and Philosophy of Science. Proceedings of the 12th International Congress, pp. 147–170. KCL Puplications (2005)

    Google Scholar 

  33. Schmidt, R., Hustadt, U.: Mechanized reasoning and model generation for extended modal logics. In: de Swart, H., Orłowska, E., Schmidt, G., Roubens, M. (eds.) Theory and Applications of Relational Structures as Knowledge Instruments. LNCS, vol. 2929, pp. 38–67. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  34. Schoenfeld, W.: Upper bounds for a proof search in a sequent calculus for relational equations. Zeitschrift fuer Mathematische Logic und Grundlagen der Mathematik 28, 239–246 (1982)

    Article  MATH  Google Scholar 

  35. Tarski, A., Givant, S.: A formalization of Set Theory without variables, Colloquium Publications. American Mathematical Society, vol. 41. Colloquium Publications (1987)

    Google Scholar 

  36. Web resources for the Tcl/Tk toolkit, http://tcl.sourceforge.net

  37. Web reference for SICStus Prolog, http://www.sics.se/sicstus

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Informatica, Università di L’Aquila, Italy

    Andrea Formisano

  2. Dipartimento di Matematica e Informatica, Università di Trieste, Italy

    Eugenio G. Omodeo

  3. National Institute of Telecommunications, Warsaw, Poland

    Ewa Orłowska

Authors
  1. Andrea Formisano
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Eugenio G. Omodeo
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Ewa Orłowska
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculty of Philosophy, Tilburg University, P.O. Box 90153, 5000, Tilburg, LE, The Netherlands

    Harrie de Swart

  2. National Institute of Telecommunications, Warsaw,  

    Ewa Orłowska

  3. Institute for Software Technology, Department of Computing Science, Universität der Bundeswehr München, 85577, Neubiberg, Germany

    Gunther Schmidt

  4. Faculté Polytechnique de Mons, Rue de Houdain 9, B-7000, Mons, Belgium

    Marc Roubens

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Formisano, A., Omodeo, E.G., Orłowska, E. (2006). An Environment for Specifying Properties of Dyadic Relations and Reasoning About Them II: Relational Presentation of Non-classical Logics. In: de Swart, H., Orłowska, E., Schmidt, G., Roubens, M. (eds) Theory and Applications of Relational Structures as Knowledge Instruments II. Lecture Notes in Computer Science(), vol 4342. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11964810_5

Download citation

  • DOI: https://doi.org/10.1007/11964810_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-69223-2

  • Online ISBN: 978-3-540-69224-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation