On the complexity of Boolean unification

DOI10.1016/S0020-0190(98)00106-9zbMath1338.68092OpenAlexW1981232804WikidataQ57383729 ScholiaQ57383729MaRDI QIDQ293360

Franz Baader

Publication date: 9 June 2016

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: http://www.sciencedirect.com/science/article/pii/S0020019098001069?np=y

zbMATH Keywords

computational complexityautomatic theorem proving

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Related Items

Algorithmic introduction of quantified cuts, Contact Logic is Finitary for Unification with Constants, Lost in translation: language independence in propositional logic -- application to belief change, Towards Parallel Boolean Functional Synthesis, Boolean functional synthesis: hardness and practical algorithms

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unification in Boolean rings and Abelian groups
• Unification in a combination of arbitrary disjoint equational theories
• Embedding Boolean expressions into logic programming
• Unification in Boolean rings
• Complexity of Boolean algebras
• Model theory.
• A resolution principle for a logic with restricted quantifiers
• Boolean unification - the story so far
• Unification in the union of disjoint equational theories: Combining decision procedures
• Two-Processor Scheduling with Start-Times and Deadlines
• Unification algorithms cannot be combined in polynomial time
• AC-superposition with constraints: No AC-unifiers needed