Abstract
Various forms of subsumption preorders are used in the literature for comparing unifiers and general solutions of a unification problem for generality and for defining the unification type. This note presents some of them and discusses their pros and cons. In particular arguments against the exist-substitution-based subsumption preorder (ess) are discussed. A proposal for a further partition of unification type nullary is made. Also some historical notes are included.
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
Similar content being viewed by others
References
Baader, F.: The theory of idempotent semigroups is of unification type zero. J. Autom. Reasoning 2(3), 283–286 (1986)
Baader, F.: Unification in commutative theories. J. Symb. Comput. 8(5), 479–497 (1989)
Baader, F.: Remarks on ACUI, personal communication (2016)
Franz, B., Borgwardt, S., Morawska, B.: Extending unification in EL to disunification: the case of dismatching and local disunification. Log. Methods Comput. Sci. 12(4) (2016)
Baader, F., Ludmann, P.: The exact unification type of commutative theories. In: Ghilardi, S., Schmidt-Schauß, M. (eds.) Informal Proceedings of the 30th International Workshop on Unification (UNIF 2016) (2016)
Baader, F., Morawska, B.: Unification in the description logic \(\cal{EL}\). In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 350–364. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02348-4_25
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Baader, F., Siekmann, J.H.: Unification theory. In: Gabbay, D.M., Hogger, C.J., Robinson, J.A., Siekmann, J.H. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming, Deduction Methodologies, vol. 2, pp. 41–126. Oxford University Press (1994)
Baader, F., Snyder, W.: Unification theory. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 2, pp. 445–532. Elsevier and MIT Press (2001)
Cabrer, L.M., Metcalfe, G.: From admissibility to a new hierarchy of unification types. In: Kutsia, T., Ringeissen, C. (eds.) Proceedings of the 28\(^{th}\) International Workshop on Unification (UNIF 2014) (2014)
Cabrer, L.M., Metcalfe, G.: Exact unification and admissibility. Log. Methods Comput. Sci. 11(3) (2015)
Calvès, C., Fernández, M.: A polynomial nominal unification algorithm. Theor. Comput. Sci. 403(2–3), 285–306 (2008)
Eder, E.: Properties of Substitutions and unifications. In: Neumann, B. (ed.) GWAI-83. Informatik-Fachberichte, vol. 76, pp. 197–206. Springer, Heidelberg (1983). https://doi.org/10.1007/978-3-642-69391-5_18
Levy, J., Villaret, M.: An efficient nominal unification algorithm. In: Lynch, C. (ed.) Proceedings of the 21st RTA, volume 6 of LIPIcs, pp. 209–226. Schloss Dagstuhl (2010)
Schmidt-Schauß, M.: Unification under associativity and idempotence is of type nullary. J. Autom. Reasoning 2(3), 277–281 (1986)
Schmidt-Schauß, M., Sabel, D., Kutz, Y.D.K.: Nominal unification with atom-variables. J. Symb. Comput. 90, 42–64 (2019)
Urban, C., Pitts, A., Gabbay, M.: Nominal unification. In: Baaz, M., Makowsky, J.A. (eds.) CSL 2003. LNCS, vol. 2803, pp. 513–527. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45220-1_41
Acknowledgements
I thank the editors, the anonymous reviewers for their help in making this paper possible, I thank the members of the orthopedics department of the hospital in Heppenheim, and my wife Marlies, for curing me and supporting me during writing.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Schmidt-Schauß, M. (2019). A Note on Unification, Subsumption and Unification Type. In: Lutz, C., Sattler, U., Tinelli, C., Turhan, AY., Wolter, F. (eds) Description Logic, Theory Combination, and All That. Lecture Notes in Computer Science(), vol 11560. Springer, Cham. https://doi.org/10.1007/978-3-030-22102-7_26
Download citation
DOI: https://doi.org/10.1007/978-3-030-22102-7_26
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-22101-0
Online ISBN: 978-3-030-22102-7
eBook Packages: Computer ScienceComputer Science (R0)