Unification in Boolean rings

DOI10.1007/BF00297246MaRDI QIDQ1112626zbMATH OpenOpenAlexWikidataFDO

Authors Tobias Nipkow, Ursula Martin Webb

Publication date 1988

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bf00297246

zbMATH Keywords

Boolean algebraBoolean ringsstring equationsunification

Mathematics Subject Classification ID

Logical aspects of Boolean algebras (03G05) Ring-theoretic properties of Boolean algebras (06E20)

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.

Recommendations

• scientific article; zbMATH DE number 4049133
• Boolean unification - the story so far
• Unification in Boolean rings and Abelian groups
• On the complexity of Boolean unification
• Unification in primal algebras, their powers and their varieties

Cites work

• A Machine-Oriented Logic Based on the Resolution Principle
• Computer-Implemented Set Theory
• Embedding Boolean expressions into logic programming
• scientific article; zbMATH DE number 3829296 (Why is no real title available?)
• scientific article; zbMATH DE number 4049130 (Why is no real title available?)
• scientific article; zbMATH DE number 4049133 (Why is no real title available?)
• scientific article; zbMATH DE number 3501560 (Why is no real title available?)
• scientific article; zbMATH DE number 3550662 (Why is no real title available?)
• scientific article; zbMATH DE number 3282724 (Why is no real title available?)
• scientific article; zbMATH DE number 3062907 (Why is no real title available?)
• New Classes for Parallel Complexity: A Study of Unification and Other Complete Problems for P
• Refutational theorem proving using term-rewriting systems
• The Knuth-Bendix Completion Procedure and Thue Systems

Cited in

(14)

• Embedding Boolean expressions into logic programming
• Hybrid terms and sentences
• Unification in free distributive lattices
• Introduction to ``Milestones in interactive theorem proving
• Finitariness of elementary unification in Boolean region connection calculus
• Boolean unification - the story so far
• Unification algorithms cannot be combined in polynomial time.
• On the complexity of Boolean unification
• Boolean unification with predicates
• scientific article; zbMATH DE number 4049133 (Why is no real title available?)
• scientific article; zbMATH DE number 16457 (Why is no real title available?)
• scientific article; zbMATH DE number 1114006 (Why is no real title available?)
• Unification in Boolean rings and Abelian groups
• An abstract fixed-point theorem for Horn formula equations

This page was built for publication: Unification in Boolean rings

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1112626)