Unification in a combination of arbitrary disjoint equational theories

DOI10.1016/S0747-7171(89)80022-7MaRDI QIDQ582270zbMATH OpenFDO

Authors Manfred Schmidt-Schauß

Publication date 1989

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

Full work available at URL https://doi.org/10.1016/S0747-7171(89)80022-7

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)

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

(50)

• 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
• Title not available (Why is no real title available?)
• 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)