@inproceedings{ddac5d33c0424733bd8f08a1114eec19,
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",
year = "1986",
doi = "10.1007/3-540-16780-3_115",
language = "English",
isbn = "978-3-540-39861-5",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "506--513",
editor = "Siekmann, {J{\"o}rg H.}",
booktitle = "8th International Conference on Automated Deduction",
address = "United Kingdom",
}