Combination techniques and decision problems for disunification

DOI10.1016/0304-3975(94)00277-0zbMath0873.68188OpenAlexW2015373596WikidataQ57383743 ScholiaQ57383743MaRDI QIDQ673624

Franz Baader, Klaus U. Schulz

Publication date: 28 February 1997

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(94)00277-0

zbMATH Keywords

combination techniquesdisunification problems

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42) Equational classes, universal algebra in model theory (03C05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (9)

Non-disjoint combined unification and closure by equational paramodulation ⋮ Symbolic Protocol Analysis with Disequality Constraints Modulo Equational Theories ⋮ Combination of constraint solvers for free and quasi-free structures ⋮ Extending Unification in $\mathcal{EL}$ to Disunification: The Case of Dismatching and Local Disunification ⋮ On solving nominal disunification constraints ⋮ Nominal equational problems ⋮ Variant-Based Satisfiability in Initial Algebras ⋮ Combination techniques for non-disjoint equational theories ⋮ Unions of non-disjoint theories and combinations of satisfiability procedures

Cites Work

• Unification in a combination of arbitrary disjoint equational theories
• Complexity of unification problems with associative-commutative operators
• A new method for undecidability proofs of first order theories
• Coding in the existential theory of concatenation
• Simplification by Cooperating Decision Procedures
• On solving equations and disequations
• All Varieties of Bands I
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Combination techniques and decision problems for disunification