Combination of constraint solving techniques: An algebraic point of view

DOI10.1007/3-540-59200-8_69MaRDI QIDQ5055842zbMATH OpenOpenAlexFDO

Authors Franz Baader, K. U. Schulz

Publication date 9 December 2022

Published in Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-59200-8_69

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Equational classes, universal algebra in model theory (03C05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Combination techniques and decision problems for disunification
• Combination techniques and decision problems for disunification
• Unification in the union of disjoint equational theories: Combining decision procedures
• Combining unification algorithms
• scientific article; zbMATH DE number 1324441

Cites work

• A resolution principle for a logic with restricted quantifiers
• AC-superposition with constraints: no AC-unifiers needed
• Combination techniques and decision problems for disunification
• Combination techniques for non-disjoint equational theories
• Combining symbolic constraint solvers on algebraic domains
• Combining unification algorithms
• Equational problems and disunification
• Generalized varieties
• scientific article; zbMATH DE number 1324441 (Why is no real title available?)
• scientific article; zbMATH DE number 1348479 (Why is no real title available?)
• scientific article; zbMATH DE number 7015114 (Why is no real title available?)
• scientific article; zbMATH DE number 1456949 (Why is no real title available?)
• scientific article; zbMATH DE number 3227055 (Why is no real title available?)
• Simplification by Cooperating Decision Procedures
• Termination of rewriting
• Unification in a combination of arbitrary disjoint equational theories

Cited in

(7)

• Combination of constraint solvers for free and quasi-free structures
• Combining symbolic constraint solvers on algebraic domains
• Unification algorithms cannot be combined in polynomial time.
• Optimisation techniques for combing constraint solvers
• scientific article; zbMATH DE number 1324441 (Why is no real title available?)
• Combination of constraint systems II: Rational amalgamation
• Structural induction in institutions

This page was built for publication: Combination of constraint solving techniques: An algebraic point of view

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