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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
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)
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)
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)
D’Agostino, G., Montanari, A., Policriti, A.: A set-theoretic translation method for polymodal logics. Journal of Automated Reasoning 3(15), 317–337 (1995)
Demri, S., Orłowska, E.: Incomplete Information: Structure, Inference, Complexity. EATCS Monographs in Theoretical Computer Science. Springer, Heidelberg (2002)
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)
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)
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)
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)
Formisano, A., Omodeo, E., Simeoni, M.: A graphical approach to relational reasoning. Electronic Notes in Theoretical Computer Science, vol. 44(3). Elsevier, Amsterdam (2001)
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)
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)
Formisano, A., Policriti, A.: T-Resolution: Refinements and Model Elimination. Journal of Automated Reasoning 22(4), 433–483 (1999)
Frias, M., Orłowska, E.: Equational reasoning in nonclassical logics. Journal of Applied Non-Classical Logics 8(1-2), 27–66 (1998)
Goranko, V.: Modal definability in enriched languages. Notre Dame Journal of Formal Logic 31, 81–105 (1990)
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)
Hennessy, M.C.B.: A proof system for the first order relational calculus. Journal of Computer and System Sciences 20, 96–110 (1980)
Hoare, C.A.R., Jifeng, H.: The weakest prespecification. Fundamenta Informaticae IX, 51–84, Part II ibidem IX, 217–252 (1986)
Humberstone, I.L.: Inaccessible worlds. Notre Dame Journal of Formal Logic 24, 346–352 (1983)
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)
Kwatinetz, M.K.: Problems of expressibility in finite languages. PhD thesis, University of California, Berkeley (1981)
Maddux, R.: A sequent calculus for relation algebras. Annals of Pure and Applied Logic 25, 73–101 (1983)
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)
Orłowska, E.: Proof system for weakest prespecification. Information Processing Letters 27, 309–313 (1988)
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)
Orłowska, E.: Relational proof systems for relevant logics. Journal of Symbolic Logic 57, 167–186 (1992)
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)
Orłowska, E.: Temporal logics in a relational framework. Time and Logic—A computational Approach, pp. 227–249. University College London Press (1995)
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)
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)
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)
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)
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)
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)
Tarski, A., Givant, S.: A formalization of Set Theory without variables, Colloquium Publications. American Mathematical Society, vol. 41. Colloquium Publications (1987)
Web resources for the Tcl/Tk toolkit, http://tcl.sourceforge.net
Web reference for SICStus Prolog, http://www.sics.se/sicstus
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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)