Name
Abstract | ||
|---|---|---|
Leaf permutative equations often appear in equational reasoning, and lead to dumb repetitions through rather trivial though profuse variants of clauses. These variants can be compacted by performing inferences modulo a theory E of leaf permutative equations, using group-theoretic constructions, as proposed in [1]. However, this requires some tasks that happen to be NP-complete (see [7]), unless restrictions are imposed on E. A natural restriction is orthogonality, which allows the use of powerful group-theoretic algorithms to solve some of the required tasks. If sufficient, this restriction is however not necessary. We therefore investigate what kind of overlapping can be allowed in E while retaining the complexity obtained under orthogonality. |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1007/978-3-540-25984-8_32 | Lecture Notes in Artificial Intelligence |
Field | DocType | Volume |
Automated reasoning,Modulo,Group theory,Computer science,Equational reasoning,Inference,Automated theorem proving,Algorithm,Orthogonality | Conference | 3097 |
ISSN | Citations | PageRank |
0302-9743 | 4 | 0.48 |
References | Authors | |
7 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Thierry Boy de la Tour | 1 | 129 | 18.99 |
| Mnacho Echenim | 2 | 95 | 15.75 |