Boolean unification - the story so far

DOI10.1016/S0747-7171(89)80013-6zbMath0682.68093MaRDI QIDQ1824411

Tobias Nipkow, Ursula Martin Webb

Publication date: 1989

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

zbMATH Keywords

unification algorithmsBoolean unification

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Abstract data types; algebraic specification (68Q65)

Related Items

On the complexity of Boolean unification, PYTHAGOREAN TRIPLES IN THE UNIFICATION THEORY OF ASSOCIATIVE AND COMMUTATIVE RINGS, Negative Boolean constraints, Running time experiments on some algorithms for solving propositional satisfiability problems, Introduction to ``Milestones in interactive theorem proving, Unification, finite duality and projectivity in varieties of Heyting algebras, Propositional calculus problems in CHIP, Algorithmic introduction of quantified cuts, The complexity of counting problems in equational matching, A new combination procedure for the word problem that generalizes fusion decidability results in modal logics, The calculus of context relations, Best solving modal equations, The unification type of the Pythagorean equation in varieties of nilpotent rings, Towards Parallel Boolean Functional Synthesis, Unification algorithms cannot be combined in polynomial time, The Evaluation and the Computational Complexity of Datalog Queries of Boolean Constraint Databases, Boolean functional synthesis: hardness and practical algorithms, Unification problem in equational theories, Unification algorithms cannot be combined in polynomial time.

Uses Software

• REVE

Cites Work

• Refutational theorem proving using term-rewriting systems
• Unification in combinations of collapse-free regular theories
• Embedding Boolean expressions into logic programming
• Unification in Boolean rings
• Graph-Based Algorithms for Boolean Function Manipulation
• New Classes for Parallel Complexity: A Study of Unification and Other Complete Problems for P
• A Machine-Oriented Logic Based on the Resolution Principle
• A Computing Procedure for Quantification Theory
• The Theory of Representation for Boolean Algebras
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item