Name
Abstract | ||
|---|---|---|
. We present an inference system for first-order constrained clauses with equalitymodulo associativity (A). Our procedure is refutationally complete and reduces to KnuthBendixcompletion modulo A in the equational case. As an essential ingredient we presentthe first ---as far as we know--- A-compatible reduction ordering total on the ground Acongruenceclasses.1 IntroductionIn some cases, in automated theorem proving special treatments for some equational subset of theaxioms are... |
Year | DOI | Venue |
|---|---|---|
1995 | 10.1007/3-540-61377-3_53 | CSL |
Keywords | Field | DocType |
theorem proving modulo associativity,first order,automated theorem proving,theorem proving | Discrete mathematics,Factor theorem,Combinatorics,Modulo,Brouwer fixed-point theorem,Automated theorem proving,Bruck–Ryser–Chowla theorem,Fundamental theorem,Gap theorem,Mathematics,Compactness theorem | Conference |
Volume | ISSN | ISBN |
1092 | 0302-9743 | 3-540-61377-3 |
Citations | PageRank | References |
4 | 0.59 | 14 |
Authors | ||
1 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Albert Rubio | 1 | 228 | 19.44 |