MPI-INF/SWS Research Reports 1991-2021

2. Number - All Departments


Solving simplifications ordering constraints

Johann, Patricia and Socher-Ambrosius, Rolf

November 1993, 16 pages.

Status: available - back from printing

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.

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},