MPI-INF Logo
MPI-INF/SWS Research Reports 1991-2021

2. Number - All Departments

MPI-I-93-256

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: https://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1993-256

Hide details for BibTeXBibTeX
@TECHREPORT{JohannSocher-Ambrosius93,
  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},
}