Multi-completion with termination tools
type: Item
instance of: scholarly article
title: Multi-completion with termination tools
zbMATH Open document ID: 1362.68253
author: Sarah Winkler
author: Haruhiko Sato
author: Aart Middeldorp
author: Masahito Kurihara
published in: Journal of Automated Reasoning
publication date: 2013-07-05T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 68Q42
zbMATH DE Number: 6184682
zbMATH Keywords: term rewriting
zbMATH Keywords: Knuth-Bendix completion
zbMATH Keywords: termination tools
zbMATH Keywords: multi-completion
describes a project that uses: AProVE
describes a project that uses: VAMPIRE
describes a project that uses: REVE
describes a project that uses: TPTP
describes a project that uses: Tyrolean
describes a project that uses: mkbTT
describes a project that uses: Slothrop
describes a project that uses: MU-TERM
MaRDI profile type: Publication
full work available at URL: s10817-012-9249-2
OpenAlex ID: W1995618662
cites work: Proving termination of context-sensitive rewriting with MU-TERM
cites work: Q4000281
cites work: Critical pair criteria for completion
cites work: Equational inference, canonical proofs, and proof orderings
cites work: Q4234323
cites work: Existence, Uniqueness, and Construction of Rewrite Systems
cites work: Q4524770
cites work: Only prime superpositions need be considered in the Knuth-Bendix completion procedure
cites work: Q5389074
cites work: Q5581665
cites work: Q3702510
cites work: Completion for multiple reduction orderings
cites work: Q4225064
cites work: Experiments with discrimination-tree indexing and path indexing for term retrieval
cites work: About the rewriting systems produced by the Knuth-Bendix completion algorithm
cites work: Paramodulation-based theorem proving
cites work: Multi-completion with Termination Tools (System Description)
cites work: Q4942621
cites work: Term indexing
cites work: Knuth-Bendix completion of theories of commuting group endomorphisms
cites work: The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
cites work: The anatomy of vampire. Implementing bottom-up procedures with code trees
cites work: Q4539595
cites work: Slothrop: Knuth-Bendix Completion with a Modern Termination Checker
cites work: Mining propositional simplification proofs for small validating clauses
cites work: Q3702509
cites work: Termination Tools in Ordered Completion
cites work: AC Completion with Termination Tools
cites work: Q5389156
DOI: 10.1007/S10817-012-9249-2
Recommended article: Multi-completion with Termination Tools (System Description)
Recommended article: Strategy compliant multi-threaded term completion
Recommended article: Termination Tools in Ordered Completion
Recommended article: Fine-grained concurrent completion
Recommended article: Q3196855
Recommended article: Q4234323
Recommended article: Termination criteria for tree automata completion
Recommended article: Multi-dimensional interpretations for termination of term rewriting
Recommended article: AC Completion with Termination Tools
Recommended article: Completion for constrained term rewriting systems
description: scientific article; zbMATH DE number 6184682