Combination techniques and decision problems for disunification
From MaRDI portal
Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Equational classes, universal algebra in model theory (03C05) Grammars and rewriting systems (68Q42) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Recommendations
Cites work
- A new method for undecidability proofs of first order theories
- All Varieties of Bands I
- Coding in the existential theory of concatenation
- Complexity of unification problems with associative-commutative operators
- General A- and AX-unification via optimized combination procedures
- scientific article; zbMATH DE number 4089320 (Why is no real title available?)
- scientific article; zbMATH DE number 4089518 (Why is no real title available?)
- scientific article; zbMATH DE number 3566230 (Why is no real title available?)
- scientific article; zbMATH DE number 599028 (Why is no real title available?)
- scientific article; zbMATH DE number 7680806 (Why is no real title available?)
- On solving equations and disequations
- Simplification by Cooperating Decision Procedures
- Unification in a combination of arbitrary disjoint equational theories
- Unification in the union of disjoint equational theories: Combining decision procedures
Cited in
(22)- Equational problems and disunification
- Combination of constraint solvers for free and quasi-free structures
- Unions of non-disjoint theories and combinations of satisfiability procedures
- On solving nominal disunification constraints
- Nominal equational problems
- Strategies for combining decision procedures
- Canonization for disjoint unions of theories
- Extending unification in \(\mathcal{EL}\) to disunification: the case of dismatching and local disunification
- Disunification for ultimately periodic interpretations
- Symbolic Protocol Analysis with Disequality Constraints Modulo Equational Theories
- \(E\)-unification with constants vs. general \(E\)-unification
- On existential theories of list concatenation
- Why combined decision problems are often intractable
- Variant-Based Satisfiability in Initial Algebras
- Combination techniques and decision problems for disunification
- Combination of constraint solving techniques: An algebraic point of view
- Combination techniques for non-disjoint equational theories
- A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method
- Canonization for disjoint unions of theories.
- Anti-pattern templates
- A nominal approach to equational problems in languages with binders
- Non-disjoint combined unification and closure by equational paramodulation
This page was built for publication: Combination techniques and decision problems for disunification
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q673624)
