Encoding dependency pair techniques and control strategies for maximal completion

DOI10.1007/978-3-319-21401-6_10MaRDI QIDQ3454089zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

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

Cited in

(3)

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

Describes a project that uses

Uses Software

• KBCV
• Slothrop
• mkbTT

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)