Abstract
Previous results for combining decision procedures for the word problem in the non-disjoint case do not apply to equational theories induced by modal logics—whose combination is not disjoint since they share the theory of Boolean algebras. Conversely, decidability results for the fusion of modal logics are strongly tailored towards the special theories at hand, and thus do not generalize to other equational theories.
In this paper, we present a new approach for combining decision procedures for the word problem in the non-disjoint case that applies to equational theories induced by modal logics, but is not restricted to them. The known fusion decidability results for modal logics are instances of our approach. However, even for equational theories induced by modal logics our results are more general since they are not restricted to so-called normal modal logics.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Baader, F., Bürckert, H.-J., Nebel, B., Nutt, W., Smolka, G.: On the expressivity of feature logics with negation, functional uncertainty, and sort equations. J. of Logic, Language and Information 2, 1–18 (1993)
Baader, F., Ghilardi, S., Tinelli, C.: A new combination procedure for the word problem that generalizes fusion decidability results in modal logics. Technical Report 03-03, Department of Computer Science, The University of Iowa (December 2003)
Baader, F., Hanschke, P.: Extensions of concept languages for a mechanical engineering application. In: Ohlbach, H.J. (ed.) GWAI 1992. LNCS, vol. 671, pp. 132–143. Springer, Heidelberg (1993)
Baader, F., Lutz, C., Sturm, H., Wolter, F.: Fusions of description logics and abstract description systems. Journal of Artificial Intelligence Research 16, 1–58 (2002)
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, United Kingdom (1998)
Baader, F., Tinelli, C.: A new approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method. In: McCune, W. (ed.) CADE 1997. LNCS, vol. 1249, pp. 19–33. Springer, Heidelberg (1997)
Baader, F., Tinelli, C.: Deciding the word problem in the union of equational theories. Information and Computation 178(2), 346–390 (2002)
Chagrov, A., Zakharyaschev, M.: Modal Logic. Oxford Logic Guides, vol. 35. Clarendon Press, Oxford (1997)
Chang, C.-C., Keisler, H.J.: Model Theory, 3rd edn. North-Holland, Amsterdam (1990)
Chellas, B.F.: Modal Logic, an Introduction. Cambridge University Press, Cambridge (1980)
Domenjoud, E., Klay, F., Ringeissen, C.: Combination techniques for nondisjoint equational theories. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 267–281. Springer, Heidelberg (1994)
Fiorentini, C., Ghilardi, S.: Combining word problems through rewriting in categories with products. Theoretical Computer Science 294, 103–149 (2003)
Ghilardi, S.: Model Theoretic Methods in Combined Constraint Satisfiability. Journal of Automated Reasoning (2004) (to appear)
Ghilardi, S., Santocanale, L.: Algebraic and model theoretic techniques for fusion decidability in modal logics. In: Y. Vardi, M., Voronkov, A. (eds.) LPAR 2003. LNCS, vol. 2850, pp. 152–166. Springer, Heidelberg (2003)
Kracht, M., Wolter, F.: Properties of independently axiomatizable bimodal logics. The Journal of Symbolic Logic 56(4), 1469–1485 (1991)
Nelson, G.: Combining satisfiability procedures by equality-sharing. In: Bledsoe, W.W., Loveland, D.W. (eds.) Automated Theorem Proving: After 25 Years, Contemporary Mathematics, vol. 29, pp. 201–211. American Mathematical Society, Providence (1984)
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. on Programming Languages and Systems 1(2), 245–257 (1979)
Nipkow, T.: Combining matching algorithms: The regular case. Journal of Symbolic Computation 12, 633–653 (1991)
Pigozzi, D.: The join of equational theories. Colloquium Mathematicum 30(1), 15–25 (1974)
Rasiowa, H.: An Algebraic Approach to Non-Classical Logics. Studies in Logic and the Foundations of Mathematics, vol. 78. North Holland, Amsterdam (1974)
Schmidt-Schauß, M.: Unification in a combination of arbitrary disjoint equational theories. Journal of Symbolic Computation 8(1-2), 51–100 (1989); Special issue on unification. Part II
Segerberg, K.: An Essay in Classical Modal Logic. Filosofiska Studier, vol. 13. Uppsala Universitet (1971)
Spaan, E.: Complexity of Modal Logics. PhD thesis, Department of Mathematics and Computer Science, University of Amsterdam, The Netherlands (1993)
Tinelli, C., Ringeissen, C.: Unions of non-disjoint theories and combinations of satisfiability procedures. Theoretical Computer Science 290(1), 291–353 (2003)
Wolter, F.: Fusions of modal logics revisited. In: Kracht, M., de Rijke, M., Wansing, H., Zakharyaschev, M. (eds.) Advances in Modal Logic, CSLI, Stanford (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baader, F., Ghilardi, S., Tinelli, C. (2004). A New Combination Procedure for the Word Problem That Generalizes Fusion Decidability Results in Modal Logics. In: Basin, D., Rusinowitch, M. (eds) Automated Reasoning. IJCAR 2004. Lecture Notes in Computer Science(), vol 3097. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-25984-8_11
Download citation
DOI: https://doi.org/10.1007/978-3-540-25984-8_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22345-0
Online ISBN: 978-3-540-25984-8
eBook Packages: Springer Book Archive