de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Report

Solving simplifications ordering constraints

MPS-Authors
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44009

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

Locator
There are no locators available
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: http://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.