Hostname: page-component-7c8c6479df-24hb2 Total loading time: 0 Render date: 2024-03-28T09:34:38.905Z Has data issue: false hasContentIssue false

Filtering unification and most general unifiers in modal logic

Published online by Cambridge University Press:  12 March 2014

Silvio Ghilardi
Affiliation:
Dipartimento di Scienze Dell'informazione, Università Degli Studi, Via Comelico 39, 20135 Milano, Italy, E-mail: ghilardi@dsi.unimi.it
Lorenzo Sacchetti
Affiliation:
Dipartimento di Scienze Dell'informazione, Università Degli Studi, Via Comelico 39, 20135 Milano, Italy, E-mail: sacchetti@dsi.unimi.it

Abstract.

We characterize (both from a syntactic and an algebraic point of view) the normal K4-logics for which unification is filtering. We also give a sufficient semantic criterion for existence of most general unifiers, covering natural extensions of K4.2+ (i.e., of the modal system obtained from K4 by adding to it, as a further axiom schemata, the modal translation of the weak excluded middle principle).

Type
Research Article
Copyright
Copyright © Association for Symbolic Logic 2004

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Baader, F., Unification in commutative theories, Journal of Symbolic Computation, vol. 8 (1989), no. 5, pp. 479497.CrossRefGoogle Scholar
[2]Baader, F. and Narendran, P., Unification of concept terms in description logics, Journal of Symbolic Computation, vol. 31 (2001), no. 3, pp. 277305.CrossRefGoogle Scholar
[3]Baader, F. and Nutt, W., Combining problems for commutative/monoidal theories: How algebra can help in equational reasoning, Journal of Applicable Algebra in Engineering, Communication and Computing, vol. 7 (1996), no. 4, pp. 309337.CrossRefGoogle Scholar
[4]Baader, F. and Snyder, W., Unification Theory, Handbook of Automated Reasoning (Robinson, A. and Voronkov, A., editors), vol. I, Elsevier/MIT, 2001, pp. 445533.CrossRefGoogle Scholar
[5]Balbes, R. and Dwinger, P., Distributive lattices, University of Missouri Press, 1974.Google Scholar
[6]Borceux, F., Handbook of categorical algebra, 3 volumes, Cambridge University Press, 1994.Google Scholar
[7]Chagrov, A. and Zakharyaschev, M., Modal logic, Oxford University Press, Oxford, 1997.CrossRefGoogle Scholar
[8]Davey, B. A. and Priestley, H. A., Introduction to lattices and order, Cambridge University Press, Cambridge, 1990.Google Scholar
[9]Fine, K., Logics containing K4. Part I, this Journal, vol. 31 (1974), pp. 3142.Google Scholar
[10]Fine, K., Logics containing K4. Part II, this Journal, vol. 31 (1985), pp. 619651.Google Scholar
[11]Ghilardi, S., Unification through projectivity, Journal of Logic and Computation, vol. 7 (1997), no. 6, pp. 733752.CrossRefGoogle Scholar
[12]Ghilardi, S., Unification in intuitionistic logic, this Journal, vol. 64 (1999), no. 2, pp. 859880.Google Scholar
[13]Ghilardi, S., Best solving modal equations, Annals of Pure and Applied Logic, vol. 102 (2000), pp. 183198.CrossRefGoogle Scholar
[14]Ghilardi, S., A resolution/tableaux algorithm for projective approximations in IPC, Logic Journal of the IGPL. Interest Group in Pure and Applied Logics, vol. 10 (2002), no. 3, pp. 229243.Google Scholar
[15]Ghilardi, S., Sheaves, Games and Modal Completions, Trends in Logic Series, Kluwer, 2002.CrossRefGoogle Scholar
[16]Ghilardi, S., Unification, finite duality and projectivity in varieties of Hey ting algebras, Annals of Pure and Applied Logic, vol. 127 (2004), pp. 99115.CrossRefGoogle Scholar
[17]Goldblatt, R. I., Metamathematics of modal logic, Reports on Mathematical Logic, (1976), no. 6, pp. 4177.Google Scholar
[18]Goldblatt, R. I., Metamathematics of modal logic. II, Reports on Mathematical Logic, (1976), no. 7, pp. 2152.Google Scholar
[19]Iemhoff, R., Towards a proof system for admissibility, Computer Science Logic 03 (Baaz, M. and Makowski, A., editors), Lecture Notes in Computer Science 2803, 2003, pp. 255270.CrossRefGoogle Scholar
[20]Jänich, K., Topology, Undergraduate Texts in Mathematics, Springer-Verlag, 1984.CrossRefGoogle Scholar
[21]MacLane, S., Categories for the working mathematician, Springer-Verlag, 1971.Google Scholar
[22]Maksimova, L. L., A classification of modal logics, Algebra i Logika, vol. 18 (1979), no. 3, pp. 328340.Google Scholar
[23]McCune, W., Solution of the Robbins problem, Journal of Automated Reasoning, vol. 19 (1997), no. 3, pp. 263276.CrossRefGoogle Scholar
[24]Nieuwenhuis, R. and Rubio, A., Paramodulation-based theorem proving, Handbook of Automated Reasoning (Robinson, A. and Voronkov, A., editors), vol. I, Elsevier/MIT, 2001, pp. 371443.CrossRefGoogle Scholar
[25]Nutt, W., Unification in monoidal theories, Proceedings of the 10th international conference on automated deduction (Stickel, M.E., editor), Lecture Notes in Computer Science, vol. 449, Springer, Berlin, 1990, pp. 618632.CrossRefGoogle Scholar
[26]Rasiowa, H., An algebraic approach to non-classical logics, North-Holland Publishing Co., Amsterdam, 1974.Google Scholar
[27]Sambin, G. and Vaccaro, V., Topology and duality in modal logic, Annals of Pure and Applied Logic, vol. 37 (1988), pp. 249296.CrossRefGoogle Scholar