Unification in boolean rings

Ursula Martin, Tobias Nipkow

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.
Original languageEnglish
Title of host publication8th International Conference on Automated Deduction
Subtitle of host publicationOxford, England, July 27–August 1, 1986 Proceedings
EditorsJörg H. Siekmann
Place of PublicationBerlin, Heidelberg
PublisherSpringer Berlin Heidelberg
Number of pages8
ISBN (Print)978-3-540-39861-5
Publication statusPublished - 1986

Publication series

NameLecture Notes in Computer Science


Dive into the research topics of 'Unification in boolean rings'. Together they form a unique fingerprint.

Cite this