Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society


Solving simplifications ordering constraints

Johann, Patricia and Socher-Ambrosius, Rolf

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.pdfMPI-I-93-256.pdfMPI-I-93-256.dvi - 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
URL to this document:
Hide details for BibTeXBibTeX
  AUTHOR = {Johann, Patricia and Socher-Ambrosius, Rolf},
  TITLE = {Solving simplifications ordering constraints},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-93-256},
  MONTH = {November},
  YEAR = {1993},
  ISSN = {0946-011X},