Multi-completion with termination tools
From MaRDI portal
Publication:352956
DOI10.1007/S10817-012-9249-2zbMATH Open1362.68253OpenAlexW1995618662MaRDI QIDQ352956FDOQ352956
Authors: Sarah Winkler, Haruhiko Sato, Aart Middeldorp, Masahito Kurihara 
Publication date: 5 July 2013
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-012-9249-2
Recommendations
- Multi-completion with Termination Tools (System Description)
- Strategy compliant multi-threaded term completion
- Termination tools in ordered completion
- Fine-grained concurrent completion
- Publication:3196855
- scientific article; zbMATH DE number 1263425
- Termination criteria for tree automata completion
- Multi-dimensional interpretations for termination of term rewriting
- AC completion with termination tools
- Completion for constrained term rewriting systems
Cites Work
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- Proving termination of context-sensitive rewriting with MU-TERM
- Slothrop: Knuth-Bendix Completion with a Modern Termination Checker
- Existence, Uniqueness, and Construction of Rewrite Systems
- Title not available (Why is that?)
- Experiments with discrimination-tree indexing and path indexing for term retrieval
- Completion for multiple reduction orderings
- Only prime superpositions need be considered in the Knuth-Bendix completion procedure
- Critical pair criteria for completion
- About the rewriting systems produced by the Knuth-Bendix completion algorithm
- The anatomy of vampire. Implementing bottom-up procedures with code trees
- Paramodulation-based theorem proving
- Term indexing
- Mining propositional simplification proofs for small validating clauses
- Multi-completion with Termination Tools (System Description)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Equational inference, canonical proofs, and proof orderings
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- AC completion with termination tools
- Maximal completion
- Title not available (Why is that?)
- Termination tools in ordered completion
- Knuth-Bendix completion of theories of commuting group endomorphisms
Cited In (8)
- Towards automated deduction in cP systems
- Normalized completion revisited
- Multi-completion with Termination Tools (System Description)
- Fine-grained concurrent completion
- Encoding dependency pair techniques and control strategies for maximal completion
- Left-Linear Completion with AC Axioms
- Termination tools in ordered completion
- AC completion with termination tools
Uses Software
This page was built for publication: Multi-completion with termination tools
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q352956)
