Cancellative Abelian monoids and related structures in refutational theorem proving. I
type: Item
instance of: scholarly article
title: Cancellative Abelian monoids and related structures in refutational theorem proving. I
zbMATH Open document ID: 1010.68166
author: Uwe Waldmann
published in: Journal of Symbolic Computation
publication date: 2003-03-23T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 20M99
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 1886762
zbMATH Keywords: AC-superposition calculi
describes a project that uses: NQTHM
describes a project that uses: REVE
MaRDI profile type: Publication
full work available at URL: jsco.2002.0536
OpenAlex ID: W2765809787
cites work: Rewrite-based Equational Theorem Proving with Selection and Simplification
cites work: Refutational theorem proving for hierarchic first-order theories
cites work: Termination of rewriting systems by polynomial interpretations and its implementation
cites work: AC-complete unification and its application to theorem proving
cites work: Q3835049
cites work: Q4385444
cites work: Q4385532
cites work: Q3996619
cites work: Theorem proving in cancellative abelian monoids (extended abstract)
cites work: Proving refutational completeness of theorem-proving strategies
cites work: Termination and completion modulo associativity, commutativity and identity
cites work: Complexity of unification problems with associative-commutative operators
cites work: Normalized rewriting: An alternative to rewriting modulo a set of equations
cites work: AC-superposition with constraints: No AC-unifiers needed
cites work: Using forcing to prove completeness of resolution and paramodulation
cites work: A general refutational completeness result for an inference procedure based on associative-commutative unification
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: Q5678447
cites work: Theorem-proving with resolution and superposition
cites work: Automated deduction with associative-commutative operators
cites work: A Practical Decision Procedure for Arithmetic with Function Symbols
cites work: Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
cites work: Superposition theorem proving for abelian groups represented as integer modules
cites work: Associative-commutative deduction with constraints
cites work: Cancellative Abelian monoids and related structures in refutational theorem proving. II
cites work: Q3789100
DOI: 10.1006/JSCO.2002.0536
description: scientific article; zbMATH DE number 1886762