Encoding Dependency Pair Techniques and Control Strategies for Maximal Completion

DOI10.1007/978-3-319-21401-6_10zbMath1465.68126OpenAlexW1411483300MaRDI QIDQ3454089

Sarah Winkler, Haruhiko Sato

Publication date: 2 December 2015

Published in: Automated Deduction - CADE-25 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-21401-6_10

zbMATH Keywords

completionterm rewritingSAT encodingdependency pairs

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

Certified equational reasoning via ordered completion ⋮ Extending Maximal Completion (Invited Talk)

Uses Software

• mkbTT
• Slothrop
• KBCV

Cites Work

• Unnamed Item
• Multi-completion with termination tools
• Knuth-Bendix completion of theories of commuting group endomorphisms
• KBO orientability
• Matrix interpretations for proving termination of term rewriting
• KBCV – Knuth-Bendix Completion Visualizer
• Proving Termination Using Recursive Path Orders and SAT Solving
• Slothrop: Knuth-Bendix Completion with a Modern Termination Checker
• Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning
• Nagoya Termination Tool
• Constraints for Argument Filterings
• Logic for Programming, Artificial Intelligence, and Reasoning

This page was built for publication: Encoding Dependency Pair Techniques and Control Strategies for Maximal Completion