MPI-I-93-256. November 1993, 16 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry
Abstract in LaTeX format:
This paper presents a decision procedure for the existential fragment of the theory of simplification oderings, which extends previous work by D. Plaisted. We consider both solvability in the given signature and solvability in an extended signature. The algorithm has cubic complexity for pure conjunctive ordering constraints in the extended signature case. However, we show that some slight extensions of the basic problem are NP-complete, for example, if the ordering is interpreted as a total simplification ordering or a lexicographic path ordering (LPO) with arbitrary precedence.
References to related material:
|To download this research report, please select the type of document that fits best your needs.||Attachement Size(s):|
|MPI-I-93-256.pdf - MPI-I-93-256.dvi||60 KBytes; 119 KBytes|
|Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView|