Encoding dependency pair techniques and control strategies for maximal completion

DOI10.1007/978-3-319-21401-6_10zbMATH Open1465.68126OpenAlexW1411483300MaRDI QIDQ3454089FDOQ3454089

Authors: Haruhiko Sato, Sarah Winkler 

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

Recommendations

• Maximal completion
• Multi-completion with termination tools
• Slothrop: Knuth-Bendix Completion with a Modern Termination Checker
• Multi-completion with Termination Tools (System Description)
• Critical pair criteria for completion

zbMATH Keywords

SAT encodingterm rewritingcompletiondependency pairs

Mathematics Subject Classification ID

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

Cites Work

• Slothrop: Knuth-Bendix Completion with a Modern Termination Checker
• KBCV – Knuth-Bendix Completion Visualizer
• Nagoya termination tool
• Inst-Gen -- a modular approach to instantiation-based automated reasoning
• Multi-completion with termination tools
• Maximal completion
• Logic for Programming, Artificial Intelligence, and Reasoning
• Knuth-Bendix completion of theories of commuting group endomorphisms
• Matrix interpretations for proving termination of term rewriting
• Proving Termination Using Recursive Path Orders and SAT Solving
• KBO orientability
• Constraints for Argument Filterings

Cited In (3)

• Extending Maximal Completion (Invited Talk)
• Certified equational reasoning via ordered completion
• MædMax: a maximal ordered completion tool

Uses Software

• mkbTT
• Slothrop
• KBCV

This page was built for publication: Encoding dependency pair techniques and control strategies for maximal completion

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