Unification in a combination of equational theories: an efficient algorithm
From MaRDI portal
Recommendations
- scientific article; zbMATH DE number 4112560
- scientific article; zbMATH DE number 3945372
- scientific article; zbMATH DE number 3866609
- scientific article; zbMATH DE number 4049131
- Term Rewriting and Applications
- Unification in a combination of arbitrary disjoint equational theories
- scientific article; zbMATH DE number 4080961
- Unification in the union of disjoint equational theories: Combining decision procedures
- Some results on equational unification
- scientific article; zbMATH DE number 3930372
Cites work
- A Machine-Oriented Logic Based on the Resolution Principle
- A Unification Algorithm for Associative-Commutative Functions
- An Efficient Unification Algorithm
- Deciding Combinations of Theories
- scientific article; zbMATH DE number 4016226 (Why is no real title available?)
- scientific article; zbMATH DE number 3885353 (Why is no real title available?)
- scientific article; zbMATH DE number 3945372 (Why is no real title available?)
- scientific article; zbMATH DE number 4049025 (Why is no real title available?)
- scientific article; zbMATH DE number 4049133 (Why is no real title available?)
- scientific article; zbMATH DE number 4080961 (Why is no real title available?)
- Matching - a special case of unification?
- Unification in Boolean rings and Abelian groups
Cited in
(27)- Narrowing based procedures for equational disunification
- AC-unification race: The system solving approach, implementation and benchmarks
- Combining unification algorithms
- Three systems for cryptographic protocol analysis
- Single versus simultaneous equational unification and equational unification for variable-permuting theories
- Unification algorithms cannot be combined in polynomial time.
- Unification in the union of disjoint equational theories: Combining decision procedures
- Rule-based unification in combined theories and the finite variant property
- Unification modulo an equality theory for equational logic programming
- scientific article; zbMATH DE number 3871334 (Why is no real title available?)
- scientific article; zbMATH DE number 3874585 (Why is no real title available?)
- Combining equational reasoning
- scientific article; zbMATH DE number 4047179 (Why is no real title available?)
- scientific article; zbMATH DE number 4049130 (Why is no real title available?)
- Formal synthesis of a unification algorithm by the deductive-tableau method
- scientific article; zbMATH DE number 4112560 (Why is no real title available?)
- scientific article; zbMATH DE number 36613 (Why is no real title available?)
- Efficient general AGH-unification
- SAT Encoding of Unification in $\mathcal{EL}$
- Modular higher-order E-unification
- More problems in rewriting
- An algorithm for the unification of fusion theories (UFT)
- Term Rewriting and Applications
- Unification in a combination of arbitrary disjoint equational theories
- Unification theory
- A combinatory logic approach to higher-order E-unification
- Rigid E-unification: NP-completeness and applications to equational matings
This page was built for publication: Unification in a combination of equational theories: an efficient algorithm
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6488538)