KBO Constraint Solving Revisited

DOI10.1007/978-3-031-43369-6_5MaRDI QIDQ6496621zbMATH OpenFDO

Authors Hendrik Leidinger, Christoph Weidenbach

Publication date 3 May 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-43369-6_5

Mathematics Subject Classification ID

Artificial intelligence (68Txx)

Recommendations

• Simple LPO constraint solving methods
• Things to know when implementing KBO
• scientific article; zbMATH DE number 1342225
• Practical algorithms for deciding path ordering constraint satisfaction.
• scientific article; zbMATH DE number 1405617

Cites work

• Congruence classes with logic variables
• Deciding Combinations of Theories
• Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories
• Fast Decision Procedures Based on Congruence Closure
• scientific article; zbMATH DE number 3639144 (Why is no real title available?)
• scientific article; zbMATH DE number 1754649 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• Orienting rewrite rules with the Knuth-Bendix order.
• SCL(EQ): SCL for first-order logic with equality
• Variations on the Common Subexpression Problem

Cited in

(1)

• Inferring RPO symbol orderings

This page was built for publication: KBO Constraint Solving Revisited

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