Combining unification algorithms

DOI10.1006/JSCO.1993.1066MaRDI QIDQ1329186zbMATH OpenOpenAlexFDO

Authors Alexandre Boudet

Publication date 18 October 1995

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

Full work available at URL https://doi.org/10.1006/jsco.1993.1066

zbMATH Keywords

unification algorithms

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Grammars and rewriting systems (68Q42)

Recommendations

• Unification in a combination of equational theories: an efficient algorithm
• scientific article; zbMATH DE number 4049130
• scientific article; zbMATH DE number 4112560
• scientific article; zbMATH DE number 1346495
• scientific article; zbMATH DE number 1552528

Cited in

(39)

• AC-complete unification and its application to theorem proving
• Unification algorithms cannot be combined in polynomial time.
• scientific article; zbMATH DE number 1722699 (Why is no real title available?)
• Average-case analysis of unification algorithms
• Combination techniques and decision problems for disunification
• scientific article; zbMATH DE number 2089363 (Why is no real title available?)
• Combination of constraint solving techniques: An algebraic point of view
• Unification algorithms cannot be combined in polynomial time
• Prototyping combination of unification algorithms with the \(\mathsf{ELAN}\) rule-based programming language
• scientific article; zbMATH DE number 3871334 (Why is no real title available?)
• scientific article; zbMATH DE number 3945372 (Why is no real title available?)
• scientific article; zbMATH DE number 4049130 (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?)
• Unification with extended patterns
• scientific article; zbMATH DE number 1552528 (Why is no real title available?)
• scientific article; zbMATH DE number 4092822 (Why is no real title available?)
• Rule-based unification in combined theories and the finite variant property
• Solutions of functional equations in Shostak theories
• Unification Modulo Builtins
• Unification in combinations of collapse-free regular theories
• Combination of constraint solvers for free and quasi-free structures
• Complexity of linear standard theories
• scientific article; zbMATH DE number 3957052 (Why is no real title available?)
• Solution of systems of equations in the first-order Shostak theories
• A practical unification algorithm
• Combining matching algorithms: The regular case
• Unions of non-disjoint theories and combinations of satisfiability procedures
• A practically efficient and almost linear unification algorithm
• An algorithm for the unification of fusion theories (UFT)
• Combination of convex theories: modularity, deduction completeness, and explanation
• Rewriting modulo SMT and open system analysis
• scientific article; zbMATH DE number 3866609 (Why is no real title available?)
• Unification and matching in hierarchical combinations of syntactic theories
• scientific article; zbMATH DE number 3952479 (Why is no real title available?)
• Variant-Based Satisfiability in Initial Algebras
• Variants and satisfiability in the infinitary unification wonderland
• scientific article; zbMATH DE number 4047179 (Why is no real title available?)
• Combining equational reasoning

This page was built for publication: Combining unification algorithms

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