Unification in a combination of arbitrary disjoint equational theories

DOI10.1016/S0747-7171(89)80022-7zbMath0691.03003MaRDI QIDQ582270

Manfred Schmidt-Schauss

Publication date: 1989

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

zbMATH Keywords

unification in a disjoint combination of regular and collapse-free equational theories

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Equational logic, Mal'tsev conditions (08B05) Equational classes, universal algebra in model theory (03C05)

Related Items (37)

Second-order unification in the presence of linear shallow algebraic equations ⋮ Non-disjoint combined unification and closure by equational paramodulation ⋮ On the complexity of Boolean unification ⋮ Adding homomorphisms to commutative/monoidal theories or how algebra can help in equational unification ⋮ Modular higher-order E-unification ⋮ More problems in rewriting ⋮ Combination of constraint solving techniques: An algebraic point of view ⋮ An algorithm for distributive unification ⋮ Combination problems for commutative/monoidal theories or how algebra can help in equational unification ⋮ Combination of constraint solvers for free and quasi-free structures ⋮ Modularity in term rewriting revisited ⋮ Unnamed Item ⋮ Deciding the word problem in the union of equational theories. ⋮ Unification and Matching in Hierarchical Combinations of Syntactic Theories ⋮ A new combination procedure for the word problem that generalizes fusion decidability results in modal logics ⋮ Decidability and combination results for two notions of knowledge in security protocols ⋮ \(E\)-unification with constants vs. general \(E\)-unification ⋮ Efficient general AGH-unification ⋮ The unification hierarchy is undecidable ⋮ Combining matching algorithms: The regular case ⋮ Modular termination of \(r\)-consistent and left-linear term rewriting systems ⋮ Combination techniques and decision problems for disunification ⋮ A combinatory logic approach to higher-order E-unification ⋮ Unification algorithms cannot be combined in polynomial time ⋮ Unification theory ⋮ Hierarchical combination of intruder theories ⋮ Combination techniques and decision problems for disunification ⋮ On interreduction of semi-complete term rewriting systems ⋮ Symbolic protocol analysis in the union of disjoint intruder theories: combining decision procedures ⋮ Using types as search keys in function libraries ⋮ AC unification through order-sorted AC1 unification ⋮ A Proof Theoretic Analysis of Intruder Theories ⋮ Unification problem in equational theories ⋮ A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method ⋮ Unions of non-disjoint theories and combinations of satisfiability procedures ⋮ Unification algorithms cannot be combined in polynomial time. ⋮ Terminating non-disjoint combined unification

Cites Work

• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unification under associativity and idempotence is of type nullary
• The theory of idempotent semigroups is of unification type zero
• Unification in Boolean rings and Abelian groups
• Matching - a special case of unification?
• Properties of substitutions and unifications
• Unification in combinations of collapse-free regular theories
• New decision algorithms for finitely presented commutative semigroups
• Combining matching algorithms: The regular case
• Linear unification
• Computational aspects of an order-sorted logic with term declarations
• Complete sets of unifiers and matchers in equational theories
• Basic narrowing revisited
• Untersuchungen über das logische Schliessen. I
• Completion of a Set of Rules Modulo a Set of Equations
• Proving termination with multiset orderings
• Simplification by Cooperating Decision Procedures
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• A Unification Algorithm for Associative-Commutative Functions
• An Efficient Unification Algorithm
• The decision problem for equational bases of algebras
• On the Church-Rosser property for the direct sum of term rewriting systems
• A Machine-Oriented Logic Based on the Resolution Principle
• The Concept of Demodulation in Theorem Proving

This page was built for publication: Unification in a combination of arbitrary disjoint equational theories