Unification in a combination of arbitrary disjoint equational theories

DOI10.1016/S0747-7171(89)80022-7zbMATH Open0691.03003MaRDI QIDQ582270FDOQ582270

Authors: Manfred Schmidt-Schauß 

Publication date: 1989

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

Recommendations

• Unification in the union of disjoint equational theories: Combining decision procedures
• Unification in combinations of collapse-free regular theories
• scientific article; zbMATH DE number 4080961
• scientific article; zbMATH DE number 1346495
• Unification in a combination of equational theories: an efficient algorithm

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 classes, universal algebra in model theory (03C05) Equational logic, Mal'tsev conditions (08B05)

Cites Work

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

Cited In (48)

• Unification algorithms cannot be combined in polynomial time.
• Modularity in term rewriting revisited
• Combination techniques and decision problems for disunification
• Non-disjoint combined unification and closure by equational paramodulation
• Adding homomorphisms to commutative/monoidal theories or how algebra can help in equational unification
• Unification theory
• Combination of constraint solving techniques: An algebraic point of view
• Unification algorithms cannot be combined in polynomial time
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Retrieving library identifiers via equational matching of types
• A Proof Theoretic Analysis of Intruder Theories
• Decidability and combination results for two notions of knowledge in security protocols
• \(E\)-unification with constants vs. general \(E\)-unification
• On the complexity of Boolean unification
• Terminating non-disjoint combined unification
• More problems in rewriting
• An algorithm for distributive unification
• Unification in combinations of collapse-free regular theories
• Combination of constraint solvers for free and quasi-free structures
• Combining matching algorithms: The regular case
• Efficient general AGH-unification
• Hierarchical combination of intruder theories
• Single versus simultaneous equational unification and equational unification for variable-permuting theories
• Deciding the word problem in the union of equational theories.
• AC unification through order-sorted AC1 unification
• Unions of non-disjoint theories and combinations of satisfiability procedures
• Combination problems for commutative/monoidal theories or how algebra can help in equational unification
• Unification in a combination of equational theories: an efficient algorithm
• Unification in the union of disjoint equational theories: Combining decision procedures
• A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method
• The unification hierarchy is undecidable
• Title not available (Why is that?)
• A new combination procedure for the word problem that generalizes fusion decidability results in modal logics
• Unification and matching in hierarchical combinations of syntactic theories
• On interreduction of semi-complete term rewriting systems
• Modular higher-order E-unification
• Using types as search keys in function libraries
• Symbolic protocol analysis in the union of disjoint intruder theories: combining decision procedures
• Term Rewriting and Applications
• Second-order unification in the presence of linear shallow algebraic equations
• Unification problem in equational theories
• On Asymmetric Unification and the Combination Problem in Disjoint Theories
• 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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q582270)