Unification in Boolean rings
type: Item
instance of: scholarly article
title: Unification in Boolean rings
zbMATH Open document ID: 0659.68111
DOI: 10.1007/BF00297246
author: Tobias Nipkow
author: Ursula Martin Webb
published in: Journal of Automated Reasoning
publication date: 1988-01-01T00:00:00Z
review text: The prime concern of this paper is a concise exposition of unification in Boolean rings using Löwenheim's method. Following a brief but instructive introduction of Boolean rings Löwenheim's theorem on unification of Boolean terms by their most general unifier is proven. Arbitrary Boolean rings can easily be transformed to represent each of its elements in terms of an orthogonal basis. This orthogonal normal form of Boolean terms constitutes the starting point of the unification algorithm that is presented here designed to lower time complexity considerably. Eventually the impact of this algorithm applied to solve unification problems in set theory as well as in propositional calculus is demonstrated by examples.
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 06E20
Mathematics Subject Classification ID: 03G05
zbMATH DE Number: 4078848
zbMATH Keywords: Boolean algebra
zbMATH Keywords: string equations
zbMATH Keywords: unification
zbMATH Keywords: Boolean rings
Wikidata QID: Q55393330
MaRDI profile type: Publication
cites work: Q5802117
cites work: Embedding Boolean expressions into logic programming
cites work: Q5569204
cites work: Q3786019
cites work: Q3674088
cites work: Refutational theorem proving using term-rewriting systems
cites work: The Knuth-Bendix Completion Procedure and Thue Systems
cites work: Q3786022
cites work: Q4124795
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: Q4083731
cites work: New Classes for Parallel Complexity: A Study of Unification and Other Complete Problems for P
cites work: Computer-Implemented Set Theory
full work available at URL: https://doi.org/10.1007/bf00297246
OpenAlex ID: W2052429743
description: scientific article; zbMATH DE number 4078848