Abstract
We introduce an Automatic Theorem Prover (ATP) of a dual tableau system for a relational logic for order of magnitude qualitative reasoning, which allows us to deal with relations such as negligibility, non-closeness and distance. Dual tableau systems are validity checkers that can serve as a tool for verification of a variety of tasks in order of magnitude reasoning, such as the use of qualitative sum of some classes of numbers. In the design of our ATP, we have introduced some heuristics, such as the so called phantom variables, which improve the efficiency of the selection of variables used un the proof.
Partially supported by Spanish projects TIN2006-15455-C03-01 and P6-FQM-02049.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Bennett, B., Cohn, A.G., Wolter, F., Zakharyaschev, M.: Multi-Dimensional Modal Logic as a Framework for Spatio-Temporal Reasoning. Applied Intelligence 17(3), 239–251 (2002)
Burrieza, A., Mora, A., Ojeda-Aciego, M., Orłowska, E.: Implementing a relational system for order-of-magnitude reasoning. Technical Report (2008)
Burrieza, A., Muñoz-Velasco, E., Ojeda-Aciego, M.: A Logic for Order of Magnitude Reasoning with Negligibility, Non-closeness and Distance. In: Borrajo, D., Castillo, L., Corchado, J.M. (eds.) CAEPIA 2007. LNCS (LNAI), vol. 4788, pp. 210–219. Springer, Heidelberg (2007)
Burrieza, A., Muñoz, E., Ojeda-Aciego, M.: Order of magnitude qualitative reasoning with bidirectional negligibility. In: Marín, R., Onaindía, E., Bugarín, A., Santos, J. (eds.) CAEPIA 2005. LNCS (LNAI), vol. 4177, pp. 370–378. Springer, Heidelberg (2006)
Burrieza, A., Ojeda-Aciego, M.: A multimodal logic approach to order of magnitude qualitative reasoning with comparability and negligibility relations. Fundamenta Informaticae 68, 21–46 (2005)
Burrieza, A., Ojeda-Aciego, M., Orłowska, E.: Relational approach to order-of-magnitude reasoning. In: de Swart, H., Orłowska, E., Schmidt, G., Roubens, M. (eds.) TARSKI 2006. LNCS (LNAI), vol. 4342, pp. 105–124. Springer, Heidelberg (2006)
Dague, P.: Symbolic reasoning with relative orders of magnitude. In: Proc. 13th Intl. Joint Conference on Artificial Intelligence, pp. 1509–1515. Morgan Kaufmann, San Francisco (1993)
Dallien, J., MacCaull, W.: RelDT: A relational dual tableaux automated theorem prover, http://www.logic.stfx.ca/reldt/
Formisano, A., Orłowska, E., Omodeo, E.: A PROLOG tool for relational translation of modal logics: A front-end for relational proof systems. In: Beckert, B. (ed.) TABLEAUX 2005 Position Papers and Tutorial Descriptions, Fachberichte Informatik No 12, Universitaet Koblenz-Landau, pp. 1–10 (2005), http://www.di.univaq.it/TARSKI/transIt/
Golińska-Pilarek, J., Muñoz-Velasco, E.: Relational approach for a logic for order of magnitude qualitative reasoning with negligibility, non-closeness and distance. Technical Report (2008)
Golińska-Pilarek, J., Orłowska, E.: Relational logics and their applications. In: de Swart, H., Orłowska, E., Schmidt, G., Roubens, M. (eds.) TARSKI 2006. LNCS (LNAI), vol. 4342, pp. 125–161. Springer, Heidelberg (2006)
MacCaull, W., Orłowska, E.: Correspondence results for relational proof systems with application to the Lambek calculus. Studia Logica 71, 279–304 (2002)
Mavrovouniotis, M.L., Stephanopoulos, G.: Reasoning with orders of magnitude and approximate relations. In: Proc. 6th National Conference on Artificial Intelligence. The AAAI Press/The MIT Press (1987)
Mavrovouniotis, M.L.: A belief framework for order-of-magnitude reasoning and other qualitative relations. Artificial Intelligence in Engineering 11(2), 121–134 (1997)
Orłowska, E.: Relational interpretation of modal logics. In: Andréka, H., Monk, D., Nemeti, I. (eds.) Algebraic Logic, Col. Math. Soc. J. Bolyai., vol. 54, pp. 443–471. North Holland, Amsterdam (1988)
Raiman, O.: Order of magnitude reasoning. Artificial Intelligence 51, 11–38 (1991)
Randell, D., Cui, Z., Cohn, A.: A spatial logic based on regions and connections. In: Proc. of the 3rd International Conference on Principles of Knowledge Representation and Reasoning (KR 1992), pp. 165–176 (1992)
Rasiowa, H., Sikorski, R.: The Mathematics of Metamathematics. Polish Scientific Publishers, Warsaw (1963)
Sánchez, M., Prats, F., Piera, N.: Una formalizacin de relaciones de comparabilidad en modelos cualitativos. Boletín de la AEPIA (Bulletin of the Spanish Association for AI) 6, 15–22 (1996)
Travé-Massuyès, L., Ironi, L., Dague, P.: Mathematical Foundations of Qualitative Reasoning. AI Magazine, American Asociation for Artificial Intelligence, 91–106 (2003)
Wolter, F., Zakharyaschev, M.: Qualitative spatio-temporal representation and reasoning: a computational perspective. In: Lakemeyer, G., Nebel, B. (eds.) Exploring Artificial Intelligence in the New Millenium. Morgan Kaufmann, San Francisco (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Golińska-Pilarek, J., Mora, A., Muñoz-Velasco, E. (2008). An ATP of a Relational Proof System for Order of Magnitude Reasoning with Negligibility, Non-closeness and Distance. In: Ho, TB., Zhou, ZH. (eds) PRICAI 2008: Trends in Artificial Intelligence. PRICAI 2008. Lecture Notes in Computer Science(), vol 5351. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-89197-0_15
Download citation
DOI: https://doi.org/10.1007/978-3-540-89197-0_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-89196-3
Online ISBN: 978-3-540-89197-0
eBook Packages: Computer ScienceComputer Science (R0)