Towards a foundation of completion procedures as semidecision procedures
type: Item
instance of: scholarly article
title: Towards a foundation of completion procedures as semidecision procedures
zbMATH Open document ID: 0873.68107
DOI: 10.1016/0304-3975(94)00187-N
author: Maria Paola Bonacina
author: Jieh Hsiang
published in: Theoretical Computer Science
publication date: 1997-02-28T00:00:00Z
Mathematics Subject Classification ID: 68Q42
zbMATH DE Number: 985391
zbMATH Keywords: confluent rewrite systems
describes a project that uses: SbReve2
MaRDI profile type: Publication
cites work: Automated proofs of the Moufang identities in alternative rings
cites work: Critical pair criteria for completion
cites work: Completion for rewriting modulo a congruence
cites work: Equational inference, canonical proofs, and proof orderings
cites work: Completion of first-order clauses with equality by strict superposition
cites work: On rewrite programs: Semantics and relationship with prolog
cites work: Q5679729
cites work: Orderings for term-rewriting systems
cites work: Computing with rewrite systems
cites work: Termination of rewriting
cites work: Q3427354
cites work: A maximal-literal unit strategy for horn clauses
cites work: Q4036569
cites work: Q4385532
cites work: Q3970984
cites work: Proving termination with multiset orderings
cites work: Q3210187
cites work: Q3338216
cites work: A strong restriction of the inductive completion procedure
cites work: Q3880309
cites work: Refutational theorem proving using term-rewriting systems
cites work: Rewrite method for theorem proving in first order theory with equality
cites work: Q3674088
cites work: Q3786024
cites work: Q3028369
cites work: Proving refutational completeness of theorem-proving strategies
cites work: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
cites work: A complete proof of correctness of the Knuth-Bendix completion algorithm
cites work: Proofs by induction in equational theories with constructors
cites work: Completion of a Set of Rules Modulo a Set of Equations
cites work: Automatic proofs by induction in theories without constructors
cites work: Proof by consistency
cites work: Q3783519
cites work: Q5581665
cites work: On word problems in Horn theories
cites work: A Technique for Establishing Completeness Results in Theorem Proving with Equality
cites work: Complete Sets of Reductions for Some Equational Theories
cites work: Semantic confluence tests and completion methods
cites work: Theorem-proving with resolution and superposition
cites work: How to avoid the derivation of redundant clauses in reasoning systems
cites work: A Unification Algorithm for Associative-Commutative Functions
cites work: Q3789100
cites work: On restrictions of ordered paramodulation with simplification
full work available at URL: 0304-3975(94)00187-n
OpenAlex ID: W2044301710
description: scientific article; zbMATH DE number 985391