Name
Abstract | ||
|---|---|---|
We describe a refined superposition calculus for cancellative abelian monoids. They encompassnot only abelian groups, but also such ubiquitous structures as the natural numbers or multisets.Both the AC axioms and the cancellation law are difficult for a general purpose superpositiontheorem prover, as they create many variants of clauses which contain sums. Our calculus requiresneither explicit inferences with the theory clauses for cancellative abelian monoids nor extendedequations or... |
Year | DOI | Venue |
|---|---|---|
1996 | 10.1007/3-540-61511-3_102 | CADE |
Keywords | Field | DocType |
theorem proving,extended abstract,cancellative abelian monoids,abelian group | Abelian group,Discrete mathematics,Natural number,Elementary abelian group,G-module,Pure mathematics,Monoid,Superposition calculus,Arithmetic of abelian varieties,Rank of an abelian group,Mathematics | Conference |
ISBN | Citations | PageRank |
3-540-61511-3 | 12 | 0.68 |
References | Authors | |
17 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Harald Ganzinger | 1 | 1513 | 155.21 |
| Uwe Waldmann | 2 | 300 | 26.30 |