English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
Add to Basket
  Local TagsRelease HistoryDetailsSummary

Released
Report

Solving simplifications ordering constraints

MPS-Authors
/persons/resource/persons44009

Socher-Ambrosius,  Rolf
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)

MPI-I-93-256.pdf
(Any fulltext), 119KB

Supplementary Material (public)
There is no public supplementary material available
Citation

Johann, P., & Socher-Ambrosius, R.(1993). Solving simplifications ordering constraints (MPI-I-93-256). Saarbrücken: Max-Planck-Institut für Informatik.


Cite as: https://hdl.handle.net/11858/00-001M-0000-0014-B4A1-D
Abstract
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.