Unification in a combination of arbitrary disjoint equational theories
From MaRDI portal
(Redirected from Publication:582270)
The paper extends the known results on unification in a disjoint combination of regular and collapse-free equational theories (which are unification-type finitary) in the sense that arbitrary theories are admissible. The general procedure described is based on the reduction of the problem to the pure unification problem with free constants and the constant-elimination problem in the composing theories. It provides an enumeration of a complete set of unifiers, even if some unification procedure for a particular theory produces an infinite complete set of unifiers. It is proved that unifiability of \(E_ 1+E_ 2+...+E_ n\) is decidable if for every \(i=1,...,n\) there exists a method to decide unification in a combination of the \(E_ i's\) with free function symbols.
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
Cites work
- A Machine-Oriented Logic Based on the Resolution Principle
- A Unification Algorithm for Associative-Commutative Functions
- An Efficient Unification Algorithm
- Basic narrowing revisited
- Combining matching algorithms: The regular case
- Complete sets of unifiers and matchers in equational theories
- Completion of a Set of Rules Modulo a Set of Equations
- Computational aspects of an order-sorted logic with term declarations
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- scientific article; zbMATH DE number 4018416 (Why is no real title available?)
- scientific article; zbMATH DE number 3885353 (Why is no real title available?)
- scientific article; zbMATH DE number 3871319 (Why is no real title available?)
- scientific article; zbMATH DE number 3871322 (Why is no real title available?)
- scientific article; zbMATH DE number 3871334 (Why is no real title available?)
- scientific article; zbMATH DE number 4155934 (Why is no real title available?)
- scientific article; zbMATH DE number 3817070 (Why is no real title available?)
- scientific article; zbMATH DE number 3829296 (Why is no real title available?)
- scientific article; zbMATH DE number 3976991 (Why is no real title available?)
- scientific article; zbMATH DE number 4041328 (Why is no real title available?)
- scientific article; zbMATH DE number 4045129 (Why is no real title available?)
- scientific article; zbMATH DE number 4049025 (Why is no real title available?)
- scientific article; zbMATH DE number 4049128 (Why is no real title available?)
- scientific article; zbMATH DE number 4049130 (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?)
- scientific article; zbMATH DE number 4112560 (Why is no real title available?)
- scientific article; zbMATH DE number 3688776 (Why is no real title available?)
- scientific article; zbMATH DE number 3751028 (Why is no real title available?)
- scientific article; zbMATH DE number 3568056 (Why is no real title available?)
- scientific article; zbMATH DE number 3591948 (Why is no real title available?)
- scientific article; zbMATH DE number 3639689 (Why is no real title available?)
- scientific article; zbMATH DE number 3299786 (Why is no real title available?)
- scientific article; zbMATH DE number 3332449 (Why is no real title available?)
- scientific article; zbMATH DE number 3413831 (Why is no real title available?)
- scientific article; zbMATH DE number 3415409 (Why is no real title available?)
- scientific article; zbMATH DE number 3019695 (Why is no real title available?)
- Linear unification
- Matching - a special case of unification?
- New decision algorithms for finitely presented commutative semigroups
- On the Church-Rosser property for the direct sum of term rewriting systems
- Properties of substitutions and unifications
- Proving termination with multiset orderings
- Simplification by Cooperating Decision Procedures
- The Concept of Demodulation in Theorem Proving
- The decision problem for equational bases of algebras
- The theory of idempotent semigroups is of unification type zero
- Unification in Boolean rings and Abelian groups
- Unification in combinations of collapse-free regular theories
- Unification under associativity and idempotence is of type nullary
- Untersuchungen über das logische Schliessen. I
Cited in
(49)- Unification in combinations of collapse-free regular theories
- Combination of constraint solvers for free and quasi-free structures
- The unification hierarchy is undecidable
- Combining matching algorithms: The regular case
- Unification problem in equational theories
- Single versus simultaneous equational unification and equational unification for variable-permuting theories
- Deciding the word problem in the union of equational theories.
- Unions of non-disjoint theories and combinations of satisfiability procedures
- Unification algorithms cannot be combined in polynomial time.
- Unification in the union of disjoint equational theories: Combining decision procedures
- Combination problems for commutative/monoidal theories or how algebra can help in equational unification
- Modularity in term rewriting revisited
- Terminating non-disjoint combined unification
- Symbolic protocol analysis in the union of disjoint intruder theories: combining decision procedures
- A new combination procedure for the word problem that generalizes fusion decidability results in modal logics
- Hierarchical combination of intruder theories
- On the complexity of Boolean unification
- Unification and matching in hierarchical combinations of syntactic theories
- scientific article; zbMATH DE number 4049025 (Why is no real title available?)
- scientific article; zbMATH DE number 4080961 (Why is no real title available?)
- scientific article; zbMATH DE number 4112560 (Why is no real title available?)
- scientific article; zbMATH DE number 1222419 (Why is no real title available?)
- scientific article; zbMATH DE number 1346495 (Why is no real title available?)
- Decidability and combination results for two notions of knowledge in security protocols
- \(E\)-unification with constants vs. general \(E\)-unification
- Efficient general AGH-unification
- Unification algorithms cannot be combined in polynomial time
- Using types as search keys in function libraries
- Superposition for lambda-free higher-order logic
- AC unification through order-sorted AC1 unification
- Adding homomorphisms to commutative/monoidal theories or how algebra can help in equational unification
- Modular higher-order E-unification
- Combination techniques and decision problems for disunification
- More problems in rewriting
- Combination of constraint solving techniques: An algebraic point of view
- An algorithm for distributive unification
- A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method
- On Asymmetric Unification and the Combination Problem in Disjoint Theories
- Term Rewriting and Applications
- Second-order unification in the presence of linear shallow algebraic equations
- A Proof Theoretic Analysis of Intruder Theories
- On interreduction of semi-complete term rewriting systems
- Unification theory
- Unification in a combination of equational theories: an efficient algorithm
- Retrieving library identifiers via equational matching of types
- 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
- Non-disjoint combined unification and closure by equational paramodulation
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)
