@inproceedings{2300e914f09648468649e289ec7c3185,
title = "Unification in boolean rings",
abstract = "A simple unification algorithm for terms containing variables, constants and the set operators intersection and symmetric difference is presented. The solution is straightforward because the algebraic structure under consideration is a boolean ring. The main part of the algorithm is finding a particular solution which is then substituted into a general formula to yield a single most general unifier. The combination with other equational theories is briefly considered but even for simple cases the extension seems non-trivial.",
author = "Ursula Martin and Tobias Nipkow",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1986.; 8th International Conference on Automated Deduction, 1986 ; Conference date: 27-07-1986 Through 01-08-1986",
year = "1986",
doi = "10.1007/3-540-16780-3_115",
language = "English",
isbn = "9783540167808",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "506--513",
editor = "Siekmann, {Jorg H.}",
booktitle = "8th International Conference on Automated Deduction - Proceedings",
}